The Complexity of Deciding Characteristic Formulae in Van Glabbeek’s Branching-Time Spectrum

Authors Luca Aceto , Antonis Achilleos , Aggeliki Chalki , Anna Ingólfsdóttir



PDF
Thumbnail PDF

File

LIPIcs.CSL.2025.26.pdf
  • Filesize: 0.83 MB
  • 18 pages

Document Identifiers

Author Details

Luca Aceto
  • Department of Computer Science, Reykjavik University, Iceland
  • Gran Sasso Science Institute, L'Aquila, Italy
Antonis Achilleos
  • Department of Computer Science, Reykjavik University, Iceland
Aggeliki Chalki
  • Department of Computer Science, Reykjavik University, Iceland
Anna Ingólfsdóttir
  • Department of Computer Science, Reykjavik University, Iceland

Acknowledgements

The authors thank the anonymous reviewers for comments that led to improvements in the paper. This paper is dedicated to the memory of Rance Cleaveland (1961-2024), who used characteristic formulae to compute behavioural relations, logically and efficiently.

Cite As Get BibTex

Luca Aceto, Antonis Achilleos, Aggeliki Chalki, and Anna Ingólfsdóttir. The Complexity of Deciding Characteristic Formulae in Van Glabbeek’s Branching-Time Spectrum. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.26

Abstract

Characteristic formulae give a complete logical description of the behaviour of processes modulo some chosen notion of behavioural semantics. They allow one to reduce equivalence or preorder checking to model checking, and are exactly the formulae in the modal logics characterizing classic behavioural equivalences and preorders for which model checking can be reduced to equivalence or preorder checking.
This paper studies the complexity of determining whether a formula is characteristic for some process in each of the logics providing modal characterizations of the simulation-based semantics in van Glabbeek’s branching-time spectrum. Since characteristic formulae in each of those logics are exactly the satisfiable and prime ones, this article presents complexity results for the satisfiability and primality problems, and investigates the boundary between modal logics for which those problems can be solved in polynomial time and those for which they become computationally hard.
Amongst other contributions, this article also studies the complexity of constructing characteristic formulae in the modal logics characterizing simulation-based semantics, both when such formulae are presented in explicit form and via systems of equations.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Complexity theory and logic
Keywords
  • Characteristic formulae
  • prime formulae
  • bisimulation
  • simulation relations
  • modal logics
  • complexity theory
  • satisfiability

Metrics

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

References

  1. Luca Aceto, Antonis Achilleos, Aggeliki Chalki, and Anna Ingólfsdóttir. The complexity of deciding characteristic formulae in van glabbeek’s branching-time spectrum. CoRR, abs/2405.13697, 2024. URL: https://doi.org/10.48550/arXiv.2405.13697.
  2. Luca Aceto, Antonis Achilleos, Adrian Francalanza, and Anna Ingólfsdóttir. The complexity of identifying characteristic formulae. J. Log. Algebraic Methods Program., 112:100529, 2020. URL: https://doi.org/10.1016/j.jlamp.2020.100529.
  3. Luca Aceto, Dario Della Monica, Ignacio Fábregas, and Anna Ingólfsdóttir. When are prime formulae characteristic? Theor. Comput. Sci., 777:3-31, 2019. URL: https://doi.org/10.1016/j.tcs.2018.12.004.
  4. Luca Aceto, Ignacio Fábregas, David de Frutos-Escrig, Anna Ingólfsdóttir, and Miguel Palomino. Graphical representation of covariant-contravariant modal formulae. In Bas Luttik and Frank Valencia, editors, Proceedings 18th International Workshop on Expressiveness in Concurrency, EXPRESS 2011, Aachen, Germany, 5th September 2011, volume 64 of EPTCS, pages 1-15, 2011. URL: https://doi.org/10.4204/EPTCS.64.1.
  5. Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, and Jiri Srba. Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, USA, 2007. Google Scholar
  6. Luca Aceto, Anna Ingólfsdóttir, Paul Blain Levy, and Joshua Sack. Characteristic formulae for fixed-point semantics: a general framework. Math. Struct. Comput. Sci., 22(2):125-173, 2012. URL: https://doi.org/10.1017/S0960129511000375.
  7. Antonis Achilleos. The completeness problem for modal logic. In Proc. of Logical Foundations of Computer Science - International Symposium, LFCS 2018, volume 10703 of Lecture Notes in Computer Science, pages 1-21. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-72056-2_1.
  8. Benjamin Bisping, David N. Jansen, and Uwe Nestmann. Deciding all behavioral equivalences at once: A game for linear-time-branching-time spectroscopy. Log. Methods Comput. Sci., 18(3), 2022. URL: https://doi.org/10.46298/lmcs-18(3:19)2022.
  9. Andreas Blass and Yuri Gurevich. On the unique satisfiability problem. Inf. Control., 55(1-3):80-88, 1982. URL: https://doi.org/10.1016/S0019-9958(82)90439-9.
  10. Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation can't be traced. J. ACM, 42(1):232-268, 1995. URL: https://doi.org/10.1145/200836.200876.
  11. Gérard Boudol and Kim Guldstrand Larsen. Graphical versus logical specifications. Theor. Comput. Sci., 106(1):3-20, 1992. URL: https://doi.org/10.1016/0304-3975(92)90276-L.
  12. Michael C. Browne, Edmund M. Clarke, and Orna Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci., 59:115-131, 1988. URL: https://doi.org/10.1016/0304-3975(88)90098-9.
  13. Jin-yi Cai, Martin Fürer, and Neil Immerman. An optimal lower bound on the number of variables for graph identification. Comb., 12(4):389-410, 1992. URL: https://doi.org/10.1007/BF01305232.
  14. Rance Cleaveland. On automatically explaining bisimulation inequivalence. In Edmund M. Clarke and Robert P. Kurshan, editors, Computer Aided Verification, 2nd International Workshop, CAV '90, volume 531 of Lecture Notes in Computer Science, pages 364-372. Springer, 1990. URL: https://doi.org/10.1007/BFb0023750.
  15. Rance Cleaveland and Bernhard Steffen. Computing behavioural relations, logically. In Javier Leach Albert, Burkhard Monien, and Mario Rodríguez-Artalejo, editors, Automata, Languages and Programming, 18th International Colloquium, ICALP91, Madrid, Spain, July 8-12, 1991, Proceedings, volume 510 of Lecture Notes in Computer Science, pages 127-138. Springer, 1991. URL: https://doi.org/10.1007/3-540-54233-7_129.
  16. David de Frutos-Escrig, Carlos Gregorio-Rodríguez, Miguel Palomino, and David Romero-Hernández. Unifying the linear time-branching time spectrum of process semantics. Log. Methods Comput. Sci., 9(2), 2013. URL: https://doi.org/10.2168/LMCS-9(2:11)2013.
  17. Rocco De Nicola and Frits W. Vaandrager. Three logics for branching bisimulation. J. ACM, 42(2):458-487, 1995. URL: https://doi.org/10.1145/201019.201032.
  18. Rodney G. Downey and Michael R. Fellows. Fixed-parameter tractability and completeness I: Basic results. SIAM J. Comput., 24(4):873-921, 1995. URL: https://doi.org/10.1137/S0097539792228228.
  19. Rodney G. Downey and Michael R. Fellows. Fundamentals of Parameterized Complexity. Texts in Computer Science. Springer, 2013. URL: https://doi.org/10.1007/978-1-4471-5559-1.
  20. Heinz-Dieter Ebbinghaus, Jörg Flum, and Wolfgang Thomas. Mathematical logic (2. ed.). Undergraduate texts in mathematics. Springer, 1994. Google Scholar
  21. Jörg Flum and Martin Grohe. Parameterized Complexity Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2006. URL: https://doi.org/10.1007/3-540-29953-X.
  22. Rob J. van Glabbeek. The linear time - branching time spectrum I. In Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors, Handbook of Process Algebra, pages 3-99. North-Holland / Elsevier, 2001. URL: https://doi.org/10.1016/b978-044482830-9/50019-9.
  23. Susanne Graf and Joseph Sifakis. A modal characterization of observational congruence on finite terms of CCS. Inf. Control., 68(1-3):125-145, 1986. URL: https://doi.org/10.1016/S0019-9958(86)80031-6.
  24. Jan Friso Groote and Frits W. Vaandrager. Structured operational semantics and bisimulation as a congruence. Inf. Comput., 100(2):202-260, 1992. URL: https://doi.org/10.1016/0890-5401(92)90013-6.
  25. Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. J. ACM, 32(1):137-161, 1985. URL: https://doi.org/10.1145/2455.2460.
  26. Sören Holmström. A refinement calculus for specifications in Hennessy-Milner logic with recursion. Formal Aspects Comput., 1(3):242-272, 1989. URL: https://doi.org/10.1007/BF01887208.
  27. Harry B. Hunt III, Daniel J. Rosenkrantz, and Thomas G. Szymanski. On the equivalence, containment, and covering problems for the regular and context-free languages. J. Comput. Syst. Sci., 12(2):222-268, 1976. URL: https://doi.org/10.1016/S0022-0000(76)80038-4.
  28. Neil Immerman. Descriptive Complexity. Springer, 1999. URL: https://doi.org/10.1007/978-1-4612-0539-5.
  29. Anna Ingolfsdottir, Jens Christian Godskesen, and Michael Zeeberg. Fra Hennessy-Milner logik til CCS-processer. Master’s thesis, Aalborg University, 1987. In Danish. Google Scholar
  30. Sandra Kiefer, Pascal Schweitzer, and Erkal Selman. Graphs identified by logics with counting. In Giuseppe F. Italiano, Giovanni Pighizzini, and Donald Sannella, editors, Mathematical Foundations of Computer Science 2015 - 40th International Symposium, MFCS 2015, Milan, Italy, August 24-28, 2015, Proceedings, Part I, volume 9234 of Lecture Notes in Computer Science, pages 319-330. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48057-1_25.
  31. Dexter Kozen. Results on the propositional μ-calculus. Theor. Comput. Sci., 27:333-354, 1983. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  32. Richard E. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput., 6(3):467-480, 1977. URL: https://doi.org/10.1137/0206033.
  33. Kim Guldstrand Larsen. Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theor. Comput. Sci., 72(2&3):265-288, 1990. URL: https://doi.org/10.1016/0304-3975(90)90038-J.
  34. Kim Guldstrand Larsen and Arne Skou. Bisimulation through probabilistic testing. Inf. Comput., 94(1):1-28, 1991. URL: https://doi.org/10.1016/0890-5401(91)90030-6.
  35. Jan Martens and Jan Friso Groote. Computing minimal distinguishing Hennessy-Milner formulas is NP-hard, but variants are tractable. In Guillermo A. Pérez and Jean-François Raskin, editors, 34th International Conference on Concurrency Theory, CONCUR 2023, volume 279 of LIPIcs, pages 32:1-32:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2023.32.
  36. Robin Milner. An algebraic definition of simulation between programs. In D. C. Cooper, editor, Proceedings of the 2nd International Joint Conference on Artificial Intelligence, IJCAI 1971, pages 481-489. William Kaufmann, 1971. URL: http://ijcai.org/Proceedings/71/Papers/044.pdf.
  37. Robin Milner. Communication and Concurrency. Prentice Hall, 1989. Google Scholar
  38. Christos H. Papadimitriou and Mihalis Yannakakis. The complexity of facets (and some facets of complexity). J. Comput. Syst. Sci., 28(2):244-259, 1984. URL: https://doi.org/10.1016/0022-0000(84)90068-0.
  39. Bernhard Steffen and Anna Ingólfsdóttir. Characteristic formulae for processes with divergence. Inf. Comput., 110(1):149-163, 1994. URL: https://doi.org/10.1006/inco.1994.1028.
  40. Wolfgang Thomas. On the Ehrenfeucht-Fraïssé game in theoretical computer science. In Marie-Claude Gaudel and Jean-Pierre Jouannaud, editors, TAPSOFT'93: Theory and Practice of Software Development, International Joint Conference CAAP/FASE, volume 668 of Lecture Notes in Computer Science, pages 559-568. Springer, 1993. URL: https://doi.org/10.1007/3-540-56610-4_89.
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