Document Open Access Logo

(Un)Decidability for History Preserving True Concurrent Logics

Authors Paolo Baldan , Alberto Carraro , Tommaso Padoan

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2021.13.pdf
  • Filesize: 0.82 MB
  • 16 pages

Document Identifiers

Author Details

Paolo Baldan
  • University of Padova, Italy
Alberto Carraro
  • ITIS Zuccante, Venezia, Italy
Tommaso Padoan
  • University of Padova, Italy

Funding

This work is supported by the Ministero dell’Universtà e della Ricerca Scientifica of Italy, under Grant No. 201784YSZ5, PRIN2017 - ASPRA.

Cite AsGet BibTex

Paolo Baldan, Alberto Carraro, and Tommaso Padoan. (Un)Decidability for History Preserving True Concurrent Logics. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.MFCS.2021.13

Abstract

We investigate the satisfiability problem for a logic for true concurrency, whose formulae predicate about events in computations and their causal (in)dependencies. Variants of such logics have been studied, with different expressiveness, corresponding to a number of true concurrent behavioural equivalences. Here we focus on a mu-calculus style logic that represents the counterpart of history-preserving (hp-)bisimilarity, a typical equivalence in the true concurrent spectrum of bisimilarities. It is known that one can decide whether or not two 1-safe Petri nets (and in general finite asynchronous transition systems) are hp-bisimilar. Moreover, for the logic that captures hp-bisimilarity the model-checking problem is decidable with respect to prime event structures satisfying suitable regularity conditions. To the best of our knowledge, the problem of satisfiability has been scarcely investigated in the realm of true concurrent logics. We show that satisfiability for the logic for hp-bisimilarity is undecidable via a reduction from domino tilings. The fragment of the logic without fixpoints, instead, turns out to be decidable. We consider these results a first step towards a more complete investigation of the satisfiability problem for true concurrent logics, which we believe to have notable solvable cases.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Modal and temporal logics
Keywords
  • Event structures
  • history-preserving bisimilarity
  • true concurrent behavioural logics
  • satisfiability
  • decidability
  • domino systems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Rajeev Alur, Doron A. Peled, and Wojciech Penczek. Model-checking of causality properties. In Proceedings of LICS'95, pages 90-100. IEEE Computer Society, 1995. Google Scholar
  2. Paolo Baldan and Alberto Carraro. A causal view on non-intereference. Fundamenta Informaticae, 140(1):1-38, 2015. Google Scholar
  3. Paolo Baldan and Silvia Crafa. A logic for true concurrency. Journal of the ACM, 61(4):24:1-24:36, 2014. Google Scholar
  4. Paolo Baldan, Barbara König, Christina Mika-Michalski, and Tommaso Padoan. Fixpoint games in continuous lattices. PACMPL, 3(POPL):26:1-26:29, 2019. Google Scholar
  5. Paolo Baldan and Tommaso Padoan. Local model checking in a logic for true concurrency. In Javier Esparza and Andrzej S. Murawski, editors, Proceedings of FoSSaCS'17, volume 10203 of LNCS, pages 407-423. Springer, 2017. Google Scholar
  6. Paolo Baldan and Tommaso Padoan. Model checking a logic for true concurrency. ACM Trans. Comput. Log., 21(4):34:1-34:49, 2020. Google Scholar
  7. Marek A. Bednarczyk. Hereditary history preserving bisimulations or what is the power of the future perfect in program logics. Technical report, Polish Academy of Sciences, 1991. Google Scholar
  8. Robert Berger. The Undecidability of the Domino Problem. Memoirs ; No 1/66. American Mathematical Society, 1966. Google Scholar
  9. Eike Best, Raymond Devillers, Astrid Kiehn, and Lucia Pomello. Fully concurrent bisimulation. Acta Informatica, 28:231-261, 1991. Google Scholar
  10. Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Universitext. Springer Berlin Heidelberg, 2001. Google Scholar
  11. J. Bradfield and S. Fröschle. Independence-friendly modal logic and true concurrency. Nordic Journal of Computing, 9(1):102-117, 2002. Google Scholar
  12. R. De Nicola and G. Ferrari. Observational logics and concurrency models. In K. V. Nori and C. E. V. Madhavan, editors, Proceedings of FST-TCS'90, volume 472 of LNCS, pages 301-315. Springer, 1990. Google Scholar
  13. Pierpaolo Degano, Rocco De Nicola, and Ugo Montanari. Partial orderings descriptions and observations of nondeterministic concurrent processes. In Jaco W. de Bakker, Willem P. de Roever, and Grzegorz Rozenberg, editors, REX Workshop, volume 354 of LNCS, pages 438-466, Heidelberg, DE, 1988. Springer. Google Scholar
  14. Marlon Dumas and Luciano García-Bañuelos. Process mining reloaded: Event structures as a unified representation of process models and event logs. In R. R. Devillers and A. Valmari, editors, Petri Nets 2015, volume 9115 of LNCS, pages 33-48. Springer, 2015. Google Scholar
  15. Azadeh Farzan and P. Madhusudan. Causal atomicity. In T. Ball and R. B. Jones, editors, Proceedings of CAV'06, volume 4144 of LNCS, pages 315-328, 2006. Google Scholar
  16. Julian Gutierrez. Logics and bisimulation games for concurrency, causality and conflict. In L. de Alfaro, editor, Proceedings of FoSSaCS'09, volume 5504 of LNCS, pages 48-62. Springer, 2009. Google Scholar
  17. Julian Gutierrez. On bisimulation and model-checking for concurrent systems with partial order semantics. PhD thesis, University of Edinburgh, 2011. Google Scholar
  18. Julian Gutierrez and Juilian C. Bradfield. Model-checking games for fixpoint logics with partial order models. In M. Bravetti and G. Zavattaro, editors, Proceedings of CONCUR'09, volume 5710 of LNCS, pages 354-368. Springer, 2009. Google Scholar
  19. Lalita Jategaonkar and Albert R. Meyer. Deciding true concurrency equivalences on safe, finite nets. Theoretical Computer Science, 154(1):107-143, 1996. Google Scholar
  20. Alan Jeffrey and James Riely. On thin air reads towards an event structures model of relaxed memory. In M. Grohe, E. Koskinen, and N. Shankar, editors, Proceedings of LICS'16, pages 759-767. ACM, 2016. Google Scholar
  21. Marcin Jurdzinski, Mogens Nielsen, and Jirí Srba. Undecidability of domino games and hhp-bisimilarity. Information and Computation, 184(2):343-368, 2003. Google Scholar
  22. Emanuel Kieronski. Results on the guarded fragment with equivalence or transitive relations. In C.-H. Luke Ong, editor, Computer Science Logic, volume 3634 of LNCS, pages 309-324. Springer, 2005. Google Scholar
  23. P. Madhusudan. Model-checking trace event structures. In Proceedings of LICS 2013, pages 371-380. IEEE Computer Society, 2003. Google Scholar
  24. Ugo Montanari and M. Pistore. Minimal transition systems for history-preserving bisimulation. In R. Reischuk and M. Morvan, editors, Proceedings of STACS'97, volume 1200 of LNCS, pages 413-425. Springer, 1997. Google Scholar
  25. Mogens Nielsen and Christian Clausen. Games and logics for a noninterleaving bisimulation. Nordic Journal of Computing, 2(2):221-249, 1995. Google Scholar
  26. Martin Otto. Two variable first-order logic over ordered domains. Journal of Symbolic Logic, 66:685-702, 1999. Google Scholar
  27. Tommaso Padoan. Relating some logics for true concurrency. In Alessandro Aldini and Marco Bernardo, editors, Proceedings of ICTCS '18, volume 2243 of CEUR Workshop Proceedings, pages 242-253. CEUR-WS.org, 2018. Google Scholar
  28. Tommaso Padoan. Tableaux, Automata and Games for True Concurrency Properties. PhD thesis, University of Padua, 2019. Google Scholar
  29. Wojciech Penczek. Branching time and partial order in temporal logics. In Time and Logic: A Computational Approach, pages 179-228. UCL Press, 1995. Google Scholar
  30. I. Phillips and I. Ulidowski. Event identifier logic. Mathematical Structures in Computer Science, 24(2):1-51, 2014. URL: https://doi.org/10.1017/S0960129513000510.
  31. Jean Pichon-Pharabod and Peter Sewell. A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. In R. Bodík and R. Majumdar, editors, Proceedings of POPL'16, pages 622-633. ACM, 2016. Google Scholar
  32. S. Pinchinat, F. Laroussinie, and Ph. Schnoebelen. Logical characterization of truly concurrent bisimulation. Technical Report 114, LIFIA-IMAG, Grenoble, 1994. Google Scholar
  33. Christian Prisacariu. Higher dimensional modal logic. CoRR, abs/1405.4100, 2014. URL: http://arxiv.org/abs/1405.4100.
  34. Alexander M. Rabinovich and Boris A. Trakhtenbrot. Behaviour structures and nets. Fundamenta Informaticae, 11:357-404, 1988. Google Scholar
  35. Wieslaw Szwast and Lidia Tendera. The guarded fragment with transitive guards. Annals of Pure and Applied Logic, 128(1):227-276, 2004. URL: https://doi.org/10.1016/j.apal.2004.01.003.
  36. P. S. Thiagarajan. Regular event structures and finite Petri nets: A conjecture. In W. Brauer, H. Ehrig, J. Karhumäki, and A. Salomaa, editors, Formal and Natural Computing - Essays Dedicated to Grzegorz Rozenberg [on occasion of his 60th birthday], volume 2300 of LNCS, pages 244-256. Springer, 2002. Google Scholar
  37. Robert J. van Glabbeek and Ursula Goltz. Refinement of actions and equivalence notions for concurrent systems. Acta Informatica, 37(4/5):229-327, 2001. Google Scholar
  38. Walter Vogler. Deciding history preserving bisimilarity. In J. Albert, B. Monien, and M. Rodríguez-Artalejo, editors, Proceedings of ICALP'91, volume 510 of LNCS, pages 495-505. Springer, 1991. Google Scholar
  39. Hao Wang. Proving theorems by pattern recognition - I. Communications of the ACM, 3(4):220-234, 1960. URL: https://doi.org/10.1145/367177.367224.
  40. Hao Wang. Proving theorems by battern recognition - II. The Bell System Technical Journal, 40(1):1-41, 1961. URL: https://doi.org/10.1002/j.1538-7305.1961.tb03975.x.
  41. Glynn Winskel. Event Structures. In W. Brauer, W. Reisig, and G. Rozenberg, editors, Petri Nets: Applications and Relationships to Other Models of Concurrency, volume 255 of LNCS, pages 325-392. Springer, 1987. Google Scholar
  42. Glynn Winskel. Events, causality and symmetry. Computer Journal, 54(1):42-57, 2011. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact