Document Open Access Logo

Tree Algebras and Bisimulation-Invariant MSO on Finite Graphs

Authors Thomas Colcombet , Amina Doumane, Denis Kuperberg

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2025.152.pdf
  • Filesize: 1 MB
  • 16 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Algebraic language theory
  • Theory of computation → Regular languages
Keywords
  • MSO
  • mu-calculus
  • finite graphs
  • bisimulation
  • tree algebra

Metrics

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

Abstract

We establish that the bisimulation invariant fragment of MSO over finite transition systems is expressively equivalent over finite transition systems to modal μ-calculus, a question that had remained open for several decades.
The proof goes by translating the question to an algebraic framework, and showing that the languages of regular trees that are recognised by finitary tree algebras whose sorts zero and one are finite are the regular ones. This corresponds for trees to a weak form of the key translation of Wilke algebras to omega-semigroup over infinite words, and was also a missing piece in the algebraic theory of regular languages of infinite trees for twenty years.

Cite As Get BibTex

Thomas Colcombet, Amina Doumane, and Denis Kuperberg. Tree Algebras and Bisimulation-Invariant MSO on Finite Graphs. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 152:1-152:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ICALP.2025.152

Author Details

Thomas Colcombet
  • CNRS, IRIF, Université Paris Cité, France
Amina Doumane
  • CNRS, LIP, ENS Lyon, France
Denis Kuperberg
  • CNRS, LIP, ENS Lyon, France

Funding

  • Kuperberg, Denis: ANR ReCiProg.

Acknowledgements

We thank Achim Blumensath for helpful discussions, proofreading this work, and finding a major mistake in a previous version of this paper (now solved).

References

  1. Peter Aczel, Jiří Adámek, and Jiří Velebil. A coalgebraic view of infinite trees and iteration. Electronic Notes in Theoretical Computer Science, 44(1):1-26, 2001. CMCS 2001, Coalgebraic Methods in Computer Science (a Satellite Event of ETAPS 2001). URL: https://doi.org/10.1016/S1571-0661(04)80900-9.
  2. Achim Blumensath. Recognisability for algebras of infinite trees. Theor. Comput. Sci., 412(29):3463-3486, 2011. URL: https://doi.org/10.1016/J.TCS.2011.02.037.
  3. Achim Blumensath. An algebraic proof of rabin’s tree theorem. Theor. Comput. Sci., 478:1-21, 2013. URL: https://doi.org/10.1016/J.TCS.2013.01.026.
  4. Achim Blumensath. The Power-Set Construction for Tree Algebras. Logical Methods in Computer Science, Volume 19, Issue 4, November 2023. URL: https://doi.org/10.46298/lmcs-19(4:9)2023.
  5. Achim Blumensath and Felix Wolf. Bisimulation invariant monadic-second order logic in the finite. Theoretical Computer Science, 823:26-43, 2020. URL: https://doi.org/10.1016/j.tcs.2020.03.001.
  6. Mikołaj Bojańczyk and Tomasz Idziaszek. Algebra for infinite forests with an application to the temporal logic EF. In Mario Bravetti and Gianluigi Zavattaro, editors, CONCUR 2009 - Concurrency Theory, 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings, volume 5710 of Lecture Notes in Computer Science, pages 131-145. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04081-8_10.
  7. Mikołaj Bojańczyk and Bartek Klin. A non-regular language of infinite trees that is recognizable by a sort-wise finite algebra. Logical Methods in Computer Science, Volume 15, Issue 4, November 2019. URL: https://doi.org/10.23638/LMCS-15(4:11)2019.
  8. Facundo Carreiro, Alessandro Facchini, Yde Venema, and Fabio Zanasi. Weak MSO: automata and expressiveness modulo bisimilarity. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 27:1-27:27. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603101.
  9. Anuj Dawar and Martin Otto. Modal characterisation theorems over special classes of frames. Annals of Pure and Applied Logic, 161(1):1-42, 2009. URL: https://doi.org/10.1016/J.APAL.2009.04.002.
  10. S. Feferman and R. Vaught. The first order properties of products of algebraic systems. Fundamenta Mathematicae, 47(1):57-103, 1959. URL: http://eudml.org/doc/213526.
  11. Helle Hvid Hansen, Clemens Kupke, and Eric Pacuit. Neighbourhood structures: Bisimilarity and basic model theory. Logical Methods in Computer Science, Volume 5, Issue 2, April 2009. URL: https://doi.org/10.2168/LMCS-5(2:2)2009.
  12. Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In J. W. de Bakker and Jan van Leeuwen, editors, Automata, Languages and Programming, 7th Colloquium, Noordweijkerhout, The Netherlands, July 14-18, 1980, Proceedings, volume 85 of Lecture Notes in Computer Science, pages 299-309. Springer, 1980. URL: https://doi.org/10.1007/3-540-10003-2_79.
  13. David Janin and Igor Walukiewicz. On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In Ugo Montanari and Vladimiro Sassone, editors, CONCUR '96, Concurrency Theory, 7th International Conference, Pisa, Italy, August 26-29, 1996, Proceedings, volume 1119 of Lecture Notes in Computer Science, pages 263-277. Springer, 1996. URL: https://doi.org/10.1007/3-540-61604-7_60.
  14. Faron Moller and Alexander Moshe Rabinovich. On the expressive power of CTL*. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 360-368. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/LICS.1999.782631.
  15. Damian Niwiński. Fixed point characterization of infinite behavior of finite-state systems. Theoretical Computer Science, 189(1):1-69, 1997. URL: https://doi.org/10.1016/S0304-3975(97)00039-X.
  16. Maximilian Pflueger, Johannes Marti, and Egor V. Kostylev. A characterisation theorem for two-way bisimulation-invariant monadic least fixpoint logic over finite structures. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024, pages 63:1-63:14. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662107.
  17. Alexander Rabinovich. On compositionality and its limitations. ACM Trans. Comput. Log., 8(1):4, 2007. URL: https://doi.org/10.1145/1182613.1182617.
  18. Eric Rosen. Modal logic over finite structures. J. Log. Lang. Inf., 6(4):427-439, 1997. URL: https://doi.org/10.1023/A:1008275906015.
  19. Saharon Shelah. The monadic theory of order. Annals of Mathematics, 102(3):379-419, 1975. Google Scholar
  20. Johan Van Benthem. Correspondence theory. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic: Volume II: Extensions of Classical Logic, pages 167-247. Springer Netherlands, Dordrecht, 1984. URL: https://doi.org/10.1007/978-94-009-6259-0_4.
  21. Thomas Wilke. Algebras for classifying regular tree languages and an application to frontier testability. In Andrzej Lingas, Rolf Karlsson, and Svante Carlsson, editors, Automata, Languages and Programming, pages 347-358, Berlin, Heidelberg, 1993. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-56939-1_85.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact