Model-checking games for Fixpoint Logics with partial order models

Julian Gutierrez, Julian Bradfield

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

11 Citations (Scopus)


We introduce model-checking games that allow local second-order power on sets of independent transitions in the underlying partial order models where the games are played. Since the one-step interleaving semantics of such models is not considered, some problems that may arise when using interleaving semantics are avoided and new decidability results for partial orders are achieved. The games are shown to be sound and complete, and therefore determined. While in the interleaving case they coincide with the local model-checking games for the μ-calculus (Lμ), in a noninterleaving setting they verify properties of Separation Fixpoint Logic (SFL), a logic that can specify in partial orders properties not expressible with Lμ. The games underpin a novel decision procedure for model-checking all temporal properties of a class of infinite and regular event structures, thus improving previous results in the literature.

Original languageEnglish
Title of host publicationCONCUR 2009 - Concurrency Theory - 20th International Conference, CONCUR 2009, Proceedings
Number of pages15
ISBN (Print)3642040802, 9783642040801
Publication statusPublished - 2009
Externally publishedYes
Event20th International Conference on Concurrency Theory, CONCUR 2009 - Bologna, Italy
Duration: 1 Sept 20094 Sept 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5710 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference20th International Conference on Concurrency Theory, CONCUR 2009


  • Hintikka game semantics
  • Modal and temporal logics
  • Model-checking games
  • Partial order models of concurrency
  • Process algebras

Cite this