Document Open Access Logo

Modal Automata: Analysing Modal Fixpoint Logics, One Step at a Time (Invited Talk)

Author Yde Venema

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CSL.2025.5.pdf
  • Filesize: 0.5 MB
  • 5 pages
HTML5 Logo HTML (experimental)
LIPIcs.CSL.2025.5.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • modal logic
  • parity automata
  • fixpoint logic
  • one-step logic

Metrics

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

Abstract

We present and investigate a general framework for studying modal fixpoint logics and some related versions of monadic second-order logic, by means of certain finite automata that operate on Kripke structures. Characteristic of these modal automata is that the co-domain of their transition function is a set of formulas of a so-called one-step logic. The motivation for taking this perspective is that if a logic is characterised by a class of modal automata, many of its properties are already determined at the level of the much simpler one-step logic.

Cite As Get BibTex

Yde Venema. Modal Automata: Analysing Modal Fixpoint Logics, One Step at a Time (Invited Talk). In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 5:1-5:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.5

Author Details

Yde Venema
  • Institute for Logic, Language and Computation, Universiteit van Amsterdam, The Netherlands

References

  1. Facundo Carreiro, Alessandro Facchini, Yde Venema, and Fabio Zanasi. The power of the weak. ACM Trans. Comput. Log., 21(2):15:1-15:47, 2020. URL: https://doi.org/10.1145/3372392.
  2. Facundo Carreiro and Yde Venema. PDL inside the μ-calculus: A syntactic and an automata-theoretic characterization. In Rajeev Goré, Barteld P. Kooi, and Agi Kurucz, editors, Advances in Modal Logic 10, invited and contributed papers from the tenth conference on "Advances in Modal Logic," held in Groningen, The Netherlands, August 5-8, 2014, pages 74-93. College Publications, 2014. URL: http://www.aiml.net/volumes/volume10/Carreiro-Venema.pdf.
  3. Giovanna D'Agostino and Marco Hollenberg. Logical questions concerning the μ-calculus: Interpolation, lyndon and los-tarski. J. Symb. Log., 65(1):310-332, 2000. URL: https://doi.org/10.2307/2586539.
  4. Sebastian Enqvist, Fatemeh Seifan, and Yde Venema. An expressive completeness theorem for coalgebraic modal mu-calculi. Log. Methods Comput. Sci., 13(2), 2017. URL: https://doi.org/10.23638/LMCS-13(2:14)2017.
  5. Sebastian Enqvist, Fatemeh Seifan, and Yde Venema. Completeness for μ-calculi: A coalgebraic approach. Ann. Pure Appl. Log., 170(5):578-641, 2019. URL: https://doi.org/10.1016/J.APAL.2018.12.004.
  6. Sebastian Enqvist and Yde Venema. Disjunctive bases: normal forms and model theory for modal logics. Log. Methods Comput. Sci., 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:30)2019.
  7. Gaëlle Fontaine and Yde Venema. Some model theory for the modal μ-calculus: syntactic characterisations of semantic properties. Log. Methods Comput. Sci., 14(1), 2018. URL: https://doi.org/10.23638/LMCS-14(1:14)2018.
  8. David Janin and Igor Walukiewicz. Automata for the modal μ-calculus and related results. In Jirí Wiedermann and Petr Hájek, editors, Mathematical Foundations of Computer Science 1995, 20th International Symposium, MFCS'95, Prague, Czech Republic, August 28 - September 1, 1995, Proceedings, volume 969 of Lecture Notes in Computer Science, pages 552-562. Springer, 1995. URL: https://doi.org/10.1007/3-540-60246-1_160.
  9. David Janin and Igor Walukiewicz. On the expressive completeness of the propositional μ-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.
  10. Johannes Marti, Fatemeh Seifan, and Yde Venema. Uniform interpolation for coalgebraic fixpoint logic. In Lawrence S. Moss and Pawel Sobocinski, editors, 6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015, June 24-26, 2015, Nijmegen, The Netherlands, volume 35 of LIPIcs, pages 238-252. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPICS.CALCO.2015.238.
  11. Yde Venema. Expressiveness modulo bisimilarity: A coalgebraic perspective. In Alexandru Baltag and Sonja Smets, editors, Johan van Benthem on Logic and Information Dynamics, pages 33-65. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-06025-5_2.
  12. Igor Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional μ-calculus. Inf. Comput., 157(1-2):142-182, 2000. URL: https://doi.org/10.1006/INCO.1999.2836.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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