Document Open Access Logo

Succinct Graph Representations of μ-Calculus Formulas

Authors Clemens Kupke, Johannes Marti, Yde Venema

PDF
Thumbnail PDF

File

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

Document Identifiers

Author Details

Clemens Kupke
  • University of Strathclyde, UK
Johannes Marti
  • University of Amsterdam, The Netherlands
Yde Venema
  • University of Amsterdam, The Netherlands

Funding

  • Kupke, Clemens: Supported by Leverhulme Trust Research Project Grant RPG-2020-232.
  • Marti, Johannes: The research of this author has been made possible by a grant from the Dutch Research Council NWO, project nr. 617.001.857.

Cite As Get BibTex

Clemens Kupke, Johannes Marti, and Yde Venema. Succinct Graph Representations of μ-Calculus Formulas. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CSL.2022.29

Abstract

Many algorithmic results on the modal mu-calculus use representations of formulas such as alternating tree automata or hierarchical equation systems. At closer inspection, these results are not always optimal, since the exact relation between the formula and its representation is not clearly understood. In particular, there has been confusion about the definition of the fundamental notion of the size of a mu-calculus formula.
We propose the notion of a parity formula as a natural way of representing a mu-calculus formula, and as a yardstick for measuring its complexity. We discuss the close connection of this concept with alternating tree automata, hierarchical equation systems and parity games. We show that well-known size measures for mu-calculus formulas correspond to a parity formula representation of the formula using its syntax tree, subformula graph or closure graph, respectively. Building on work by Bruse, Friedmann & Lange we argue that for optimal complexity results one needs to work with the closure graph, and thus define the size of a formula in terms of its Fischer-Ladner closure. As a new observation, we show that the common assumption of a formula being clean, that is, with every variable bound in at most one subformula, incurs an exponential blow-up of the size of the closure.
To realise the optimal upper complexity bound of model checking for all formulas, our main result is to provide a construction of a parity formula that (a) is based on the closure graph of a given formula, (b) preserves the alternation-depth but (c) does not assume the input formula to be clean.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Logic and verification
Keywords
  • modal mu-calculus
  • model checking
  • alternating tree automata
  • hierachical equation systems

Metrics

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

Related Versions

References

  1. B. Afshari and G. Leigh. Cut-free completeness for modal mu-calculus. In Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic In Computer Science (LICS'17), pages 1-12. IEEE Computer Society, 2017. Google Scholar
  2. A. Arnold and D. Niwiński. Rudiments of μ-calculus, volume 146 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam, 2001. Google Scholar
  3. D. Baelde, A. Doumane, and A. Saurin. Infinitary proof theory: the multiplicative additive case. In J.-M. Talbot and L. Regnier, editors, Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, volume 62 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. Google Scholar
  4. J. Bradfield and C. Stirling. Modal μ-calculi. In J. van Benthem, P. Blackburn, and F. Wolter, editors, Handbook of Modal Logic, pages 721-756. Elsevier, 2006. Google Scholar
  5. J.C. Bradfield and I. Walukiewicz. The mu-calculus and model checking. In E. M. Clarke, Th.A. Henzinger, H. Veith, and R. Bloem, editors, Handbook of Model Checking, pages 871-919. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_26.
  6. F. Bruse, O. Friedmann, and M. Lange. On guarded transformation in the modal μ-calculus. Logic Journal of the IGPL, 23(2):194-216, 2015. Google Scholar
  7. C.S. Calude, S. Jain, B. Khoussainov, W. Li, and F. Stephan. Deciding parity games in quasipolynomial time. In H. Hatami, P. McKenzie, and V. King, editors, Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, (STOC 2017), pages 252-263, 2017. Google Scholar
  8. G. D'Agostino and M. Hollenberg. Logical questions concerning the μ-calculus. Journal of Symbolic Logic, 65:310-332, 2000. Google Scholar
  9. S. Demri, V. Goranko, and M. Lange. Temporal Logics in Computer Science: Finite-State Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. Google Scholar
  10. E.A. Emerson and C.S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In Proceedings of the 32nd Symposium on the Foundations of Computer Science, pages 368-377. IEEE Computer Society Press, 1991. Google Scholar
  11. G. Fontaine and Y. Venema. Some model theory for the modal mu-calculus: syntactic characterizations of semantic properties. Logical Methods in Computer Science, 14(1), 2018. Google Scholar
  12. E. Grädel, W. Thomas, and T. Wilke, editors. Automata, Logic, and Infinite Games, volume 2500 of LNCS. Springer, 2002. Google Scholar
  13. D. Janin and I. Walukiewicz. On the expressive completeness of the propositional μ-calculus w.r.t. monadic second-order logic. In Proceedings of the Seventh International Conference on Concurrency Theory, CONCUR '96, volume 1119 of LNCS, pages 263-277, 1996. Google Scholar
  14. D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333-354, 1983. Google Scholar
  15. C. Kupke, J. Marti, and Y. Venema. Size matters in the modal μ-calculus, 2020. URL: http://arxiv.org/abs/2010.14430.
  16. D. Niwiński. On fixed point clones. In L. Kott, editor, Proceedings of the 13th International Colloquium on Automata, Languages and Programming (ICALP 13), volume 226 of LNCS, pages 464-473, 1986. Google Scholar
  17. D. Niwiński. Fixed point characterization of infinite behavior of finite-state systems. Theoretical Computer Science, 189:1-69, 1997. Google Scholar
  18. H. Seidl and A. Neumann. On guarding nested fixpoints. In Proceedings of the 13th EACSL Annual Conference on Computer Science Logic, CSL '99, pages 484-498, 1999. Google Scholar
  19. I. Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional μ-calculus. Information and Computation, 157:142-182, 2000. Google Scholar
  20. T. Wilke. Alternating tree automata, parity games, and modal μ-calculus. Bulletin of the Belgian Mathematical Society, 8:359-391, 2001. 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 About DROPS Imprint Privacy Contact