Deciding the First Levels of the Modal mu Alternation Hierarchy by Formula Construction

Authors Karoliina Lehtinen, Sandra Quickert

Thumbnail PDF


  • Filesize: 487 kB
  • 15 pages

Document Identifiers

Author Details

Karoliina Lehtinen
Sandra Quickert

Cite AsGet BibTex

Karoliina Lehtinen and Sandra Quickert. Deciding the First Levels of the Modal mu Alternation Hierarchy by Formula Construction. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 457-471, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


We construct, for any sentence of the modal mu calculus Psi, derived sentences in the modal fragment and the fragment without least fixpoints of the modal mu calculus such that Psi is equivalent to a formula in these fragments if and only if it is equivalent to these formulas. The formula without greatest fixpoints that Psi is equivalent to if and only if it is equivalent to any formula without greatest fixpoint is obtained by duality. This yields a constructive proof of decidability of the first levels of the modal mu alternation hierarchy. The blow-up incurred by turning Psi into the modal formula is shown to be necessary: there are modal formulas that can be expressed sub-exponentially more efficiently with the use of fixpoints. For the fragments with only greatest or least fixpoints however, as long as formulas are in disjunctive form, the transformation into a formula syntactically in these fragments does not increase the size of the formula.
  • modal mu calculus
  • fixpoint logic
  • alternation hierarchy


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


  1. J.C. Bradfield. The modal mu-calculus alternation hierarchy is strict. In Ugo Montanari and Vladimiro Sassone, editors, CONCUR'96: Concurrency Theory, volume 1119 of Lecture Notes in Computer Science, pages 233-246. Springer Berlin Heidelberg, 1996. Google Scholar
  2. J.C. Bradfield and C. Stirling. Modal mu-calculi. Handbook of modal logic, 3:721-756, 2007. Google Scholar
  3. E. A. Emerson and C. S. Jutla. Tree automata, mu-calculus and determinacy. In Foundations of Computer Science, 1991. Proceedings., 32nd Annual Symposium on, pages 368-377. IEEE, 1991. Google Scholar
  4. D. Janin and I. Walukiewicz. Automata for the modal μ-calculus and related results. In Proc. MFCS'95 LNCS 969, pages 552-562, 1995. Google Scholar
  5. D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27(3):333-354, 1983. Special Issue Ninth International Colloquium on Automata, Languages and Programming (ICALP) Aarhus, Summer 1982. Google Scholar
  6. D. Kozen. A finite model theorem for the propositional μ-calculus. Studia Logica, 47(3):233-241, 1988. Google Scholar
  7. O. Kupferman, M. Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM (JACM), 47(2):312-360, 2000. Google Scholar
  8. R. Küsters and T. Wilke. Deciding the first level of the μ-calculus alternation hierarchy. In Proc. FSTTCS 2002, LNCS 2556, page 241–252, 2002. Google Scholar
  9. R. Küsters and T. Wilke. Deciding the First Level of the μ-calculus Alternation Hierarchy. Technical Report 0209, Institut für Informatik und Praktische Mathematik, CAU Kiel, Germany, 2002. Google Scholar
  10. G. Lenzi. A hierarchy theorem for the μ-calculus. In Friedhelm Meyer and Burkhard Monien, editors, Automata, Languages and Programming, volume 1099 of Lecture Notes in Computer Science, pages 87-97. Springer Berlin Heidelberg, 1996. Google Scholar
  11. R. Mateescu. Local model-checking of modal mu-calculus on acyclic labeled transition systems. In Joost-Pieter Katoen and Perdita Stevens, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 2280 of Lecture Notes in Computer Science, pages 281-295. Springer Berlin Heidelberg, 2002. Google Scholar
  12. M. Nair. A new method in elementary prime number theory. Journal of the London Mathematical Society, 2(3):385-391, 1982. Google Scholar
  13. M. Otto. Eliminating recursion in the μ-calculus. In STACS 99, pages 531-540. Springer, 1999. Google Scholar
  14. I. Walukiewicz. Completeness of Kozen’s Axiomatisation of the Propositional μ-Calculus. Information and Computation, 157(1–2):142-182, 2000. Google Scholar