Abstract
Most games for analysing concurrent systems are played on interleaving models, such as graphs or infinite trees. However, several concurrent systems have partial order models rather than interleaving ones. As a consequence, a potentially algorithmically undesirable translation from a partial order setting to an interleaving one is required before analysing them with traditional techniques. In order to address this problem, this paper studies a game played directly on partial orders and describes some of its algorithmic applications. The game provides a unified approach to system and property verification which applies to different decision problems and models of concurrency. Since this framework uses partial orders to give a uniform representation of concurrent systems, logical specifications, and problem descriptions, it is particularly suitable for reasoning about concurrent systems with partial order semantics, such as Petri nets or event structures. Two applications can be cast within this unified approach: bisimulation and model-checking.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abramsky, S.: Event domains, stable functions and proof-nets. Electronic Notes in Theoretical Computer Science 172, 33–67 (2007)
Abramsky, S., Melliès, P.A.: Concurrent games and full completeness. In: LICS, pp. 431–442. IEEE Computer Society, Los Alamitos (1999)
Alfaro, L.D., Henzinger, T.A.: Concurrent omega-regular games. In: LICS, pp. 141–154. IEEE Computer Society, Los Alamitos (2000)
Alfaro, L.D., Henzinger, T.A., Kupferman, O.: Concurrent reachability games. Theoretical Computer Science 386(3), 188–217 (2007)
Benthem, J.V.: Logic games, from tools to models of interaction. In: Logic at the Crossroads, pp. 283–317. Allied Publishers (2007)
Bradfield, J.C., Stirling, C.: Modal mu-calculi. In: Handbook of Modal Logic, pp. 721–756. Elsevier, Amsterdam (2007)
Esparza, J., Heljanko, K.: Unfoldings - A Partial-Order Approach to Model Checking. EATCS Monographs in Theoretical Computer Science. Springer, Heidelberg (2008)
Ghica, D.R.: Applications of game semantics: From program analysis to hardware synthesis. In: LICS, pp. 17–26. IEEE Computer Society, Los Alamitos (2009)
Girard, J.Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. LNCS, vol. 1032. Springer, Heidelberg (1996)
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)
Gutierrez, J.: On Bisimulation and Model-Checking for Concurrent Systems with Partial Order Semantics. Ph.D. thesis, University of Edinburgh (2011)
Gutierrez, J., Bradfield, J.C.: Model-checking games for fixpoint logics with partial order models. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 354–368. Springer, Heidelberg (2009)
Martin, D.A.: Borel determinacy. Annals of Mathematics 102(2), 363–371 (1975)
Nielsen, M., Winskel, G.: Models for concurrency. In: Handbook of Logic in Computer Science, pp. 1–148. Oxford University Press, Oxford (1995)
Stirling, C.: Bisimulation, modal logic and model checking games. Logic Journal of the IGPL 7(1), 103–124 (1999)
Walukiewicz, I.: A landscape with games in the background. In: LICS, pp. 356–366. IEEE Computer Society, Los Alamitos (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gutierrez, J. (2011). Concurrent Logic Games on Partial Orders. In: Beklemishev, L.D., de Queiroz, R. (eds) Logic, Language, Information and Computation. WoLLIC 2011. Lecture Notes in Computer Science(), vol 6642. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20920-8_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-20920-8_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20919-2
Online ISBN: 978-3-642-20920-8
eBook Packages: Computer ScienceComputer Science (R0)