Abstract
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bradfield, J., Stirling, C.: Modal mu-calculi. In: Handbook of Modal Logic, vol. 3, pp. 721–756. Elsevier, Amsterdam (2006)
Grädel, E.: Model checking games. Electr. Notes Theor. Comput. Sci. 67 (2002)
Gutierrez, J.: Logics and bisimulation games for concurrency, causality and conflict. In: de Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 48–62. Springer, Heidelberg (2009)
Joyal, A., Nielsen, M., Winskel, G.: Bisimulation from open maps. Inf. Comput. 127(2), 164–185 (1996)
Madhusudan, P.: Model-checking trace event structures. In: LICS, pp. 371–380. IEEE Computer Society, Los Alamitos (2003)
Nielsen, M., Winskel, G.: Models for concurrency. In: Handbook of Logic in Computer Science, vol. 4, pp. 1–148. Oxford University Press, Oxford (1995)
Penczek, W.: Model-checking for a subclass of event structures. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 145–164. Springer, Heidelberg (1997)
Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE Computer Society, Los Alamitos (2002)
Stirling, C.: Local model checking games. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 1–11. Springer, Heidelberg (1995)
Stirling, C.: Modal and Temporal Properties of Processes. LNCS. Springer, Heidelberg (2001)
Thiagarajan, P.S.: Regular trace event structures. Technical report, BRICS (1996)
Winskel, G.: Event structure semantics for ccs and related languages. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol. 140, pp. 561–576. Springer, Heidelberg (1982)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gutierrez, J., Bradfield, J. (2009). Model-Checking Games for Fixpoint Logics with Partial Order Models. In: Bravetti, M., Zavattaro, G. (eds) CONCUR 2009 - Concurrency Theory. CONCUR 2009. Lecture Notes in Computer Science, vol 5710. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04081-8_24
Download citation
DOI: https://doi.org/10.1007/978-3-642-04081-8_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04080-1
Online ISBN: 978-3-642-04081-8
eBook Packages: Computer ScienceComputer Science (R0)