Abstract
Based on a simple axiomatization of concurrent behaviour we define two ways of observing parallel computations and show that in each case they are dual to conflict and causality, respectively. We give a logical characterization to those dualities and show that natural fixpoint modal logics can be extracted from such a characterization. We also study the equivalences induced by such logics and prove that they are decidable and can be related with well-known bisimulations for interleaving and noninterleaving concurrency. Moreover, by giving a game-theoretical characterization to the equivalence induced by the main logic, which is called Separation Fixpoint Logic (SFL), we show that the equivalence SFL induces is strictly stronger than a history-preserving bisimulation (hpb) and strictly weaker than a hereditary history-preserving bisimulation (hhpb). Our study considers branching-time models of concurrency based on transition systems and petri net structures.
Chapter PDF
Similar content being viewed by others
Keywords
References
Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)
Alur, R., Peled, D., Penczek, W.: Model-Checking of Causality Properties. In: LICS, pp. 90–100. IEEE Computer Society, Los Alamitos (1995)
Bradfield, J.: Truth and Games: Essays in Honour of Gabriel Sandu. In: Aho, T., Pietarinen, A. (eds.) Acta Philosophica Fennica. Independence: Logics and Concurrency, vol. 78, pp. 47–70. Phil. Soc. of Finland (2006)
Bradfield, J., Esparza, J., Mader, A.: A Causal Fixpoint Logic. Unpub. (1997)
Bradfield, J., Fröschle, S.: Independence-Friendly Modal Logic and True Concurrency. Nord. J. Comput. 9(1), 102–117 (2002)
Brookes, S.: A semantics for concurrent separation logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 16–34. Springer, Heidelberg (2004)
Fecher, H.: A Completed Hierarchy of True Concurrent Equivalences. Inf. Process. Lett. 89(5), 261–265 (2004)
Fröschle, S.: The Decidability Border of Hereditary History Preserving Bisimilarity. Inf. Process. Lett. 93(6), 289–293 (2005)
Fröschle, S., Hildebrandt, T.: On Plain and Hereditary History-Preserving Bisimulation. In: Kutyłowski, M., Wierzbicki, T., Pacholski, L. (eds.) MFCS 1999. LNCS, vol. 1672, pp. 354–365. Springer, Heidelberg (1999)
Glabbeek, R., Goltz, U.: Refinement of Actions and Equivalence Notions for Concurrent Systems. Acta Inf. 37(4/5), 229–327 (2001)
Hayman, J., Winskel, G.: Independence and Concurrent Separation Logic. In: LICS, pp. 147–156. IEEE Computer Society, Los Alamitos (2006)
Hennessy, M., Milner, R.: Algebraic Laws for Nondeterminism and Concurrency. J. ACM 32(1), 137–161 (1985)
Joyal, A., Nielsen, M., Winskel, G.: Bisimulation from Open Maps. Inf. Comput. 127(2), 164–185 (1996)
Mazurkiewicz, A.: Trace Theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 255, pp. 279–324. Springer, Heidelberg (1987)
Nielsen, M., Clausen, C.: Games and Logics for a Noninterleaving Bisimulation. Nord. J. Comput. 2(2), 221–249 (1995)
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.: Branching Time and Partial Order in Temporal Logics. In: Time and Logic: A Computational Approach, pp. 179–228. UCL Press (1995)
Pym, D., Tofts, C.: A Calculus and Logic of Resources and Processes. Formal Asp. Comput. 18(4), 495–517 (2006)
Reynolds, J.: Separation Logic: A Logic for Shared Mutable Data Structures. In: LICS, pp. 55–74. IEEE Computer Society, Los Alamitos (2002)
Sims, É.-J.: Extending Separation Logic with Fixpoints and Postponed Substitution. Theor. Comput. Sci. 351(2), 258–275 (2006)
Stirling, C.: Modal and Temporal Properties of Processes. Springer, Heidelberg (2001)
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. (2009). Logics and Bisimulation Games for Concurrency, Causality and Conflict. In: de Alfaro, L. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2009. Lecture Notes in Computer Science, vol 5504. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00596-1_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-00596-1_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00595-4
Online ISBN: 978-3-642-00596-1
eBook Packages: Computer ScienceComputer Science (R0)