Sciweavers

Share
CONCUR
2009
Springer

Model-Checking Games for Fixpoint Logics with Partial Order Models

11 years 6 months ago
Model-Checking Games for Fixpoint Logics with Partial Order Models
Abstract. We introduce model-checking games that allow local secondorder 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.
Julian Gutierrez, Julian C. Bradfield
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where CONCUR
Authors Julian Gutierrez, Julian C. Bradfield
Comments (0)
books