Model-checking games for fixpoint logics with partial order models

Julian Gutierrez, Julian Bradfield

Research output: Contribution to journalArticlepeer-review

Abstract

In this paper, 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 interleaving semantics of such models is not considered, some problems that may arise when using interleaving representations are avoided and new decidability results for partial order models of concurrency 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, in a partial order setting they verify properties of a number of fixpoint modal logics that can specify, in concurrent systems with partial order semantics, several properties not expressible with the μ-calculus. The games underpin a novel decision procedure for model-checking all temporal properties of a class of infinite and regular event structures, thus improving, in terms of temporal expressive power, previous results in the literature.
Original languageEnglish
Pages (from-to)766-781
Number of pages16
JournalInformation and Computation
Volume209
Issue number5
DOIs
Publication statusPublished - May 2011

Keywords

  • Fixpoint modal logics
  • Model-checking games
  • Concurrency

Fingerprint Dive into the research topics of 'Model-checking games for fixpoint logics with partial order models'. Together they form a unique fingerprint.

Cite this