Games for Logics with Partial Order Models

Abstract
Model-checking games for modal and temporal logics are played by a Verifier (exists) and a Falsifier (forall) in a formula phi and a mathematical model M, so as to determine whether or not phi is satisfied in M. In such games both players are allowed to pick single elements of the structure M, even when dealing with partial order models since a one-step interleaving semantics can be considered. However, this simplification may have undesirable effects. In order to avoid them, here we take a more direct approach. We define model-checking games where both players are able to choose sets of independent elements of the structure at hand. Such games naturally appear when studying true-concurrency systems, where sets of parallel actions can be recognised. We define infinite model-checking games in which properties about concurrency, causality and conflict can be verified. While in an interleaving case these games coincide with Stirling local model-checking games for the mu-calculus, in a noninterleaving setting they can be used to give sound and complete Hintikka style game semantics to a number of Fixpoint Logics with partial order models. Our study considers both finite and infinite state concurrent systems.