Hintikka Games for Model-Checking Partial Order Models of Concurrency

Abstract
In this talk I will present a class of model-checking games that allows 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 mu-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 mu-calculus. In particular, the games underpin a novel decision procedure for model-checking so-called temporal true-concurrency properties of a class of infinite and regular event structures.