Skip to main content
SpringerLink
Log in
Book cover

Conference on Computability in Europe

CiE 2017: Unveiling Dynamics and Complexity pp 292–303Cite as

\(\varSigma ^{\mu }_2\) is decidable for \(\varPi ^{\mu }_2\)

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10307))

Abstract

Given a \(\varPi ^{\mu }_2\) formula of the modal \(\mu \) calculus, it is decidable whether it is equivalent to a \(\varSigma ^{\mu }_2\) formula.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    assuming \(| Act |=2\); otherwise trees with one successor per label.

References

  1. Arnold, A.: The \(\mu \)-calculus alternation-depth hierarchy is strict on binary trees. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 33(4–5), 329–339 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  2. Bradfield, J.C., Stirling, C.: Modal mu-calculi. Handbook of modal logic 3, 721–756 (2007)

    Article  Google Scholar 

  3. Bradfield, J.C.: The modal mu-calculus alternation hierarchy is strict. In: Montanari, U., Sassone, V. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 233–246. Springer, Heidelberg (1996). doi:10.1007/3-540-61604-7_58

    Chapter  Google Scholar 

  4. Colcombet, T., Kuperberg, D., Löding, C., Vanden Boom, M.: Deciding the weak definability of Büchi definable tree languages. In: LIPIcs-Leibniz International Proceedings in Informatics, vol. 23. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2013)

    Google Scholar 

  5. Colcombet, T., Löding, C.: The non-deterministic mostowski hierarchy and distance-parity automata. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008. LNCS, vol. 5126, pp. 398–409. Springer, Heidelberg (2008). doi:10.1007/978-3-540-70583-3_33

    Chapter  Google Scholar 

  6. Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Proceedings of the 32nd Annual Symposium on Foundations of Computer Science, FoCS 1991, pp. 368–377. IEEE Computer Society Press (1991)

    Google Scholar 

  7. Facchini, A., Murlak, F., Skrzypczak, M.: Rabin-mostowski index problem: a step beyond deterministic automata. In: Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, pp. 499–508. IEEE Computer Society (2013)

    Google Scholar 

  8. Janin, D., Walukiewicz, I.: Automata for the modal \(\mu \)-calculus and related results. In: Wiedermann, J., Hájek, P. (eds.) MFCS 1995. LNCS, vol. 969, pp. 552–562. Springer, Heidelberg (1995). doi:10.1007/3-540-60246-1_160

    Chapter  Google Scholar 

  9. Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM (JACM) 47(2), 312–360 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  10. Küsters, R., Wilke, T.: Deciding the first level of the \(\mu \)-calculus alternation hierarchy. In: Agrawal, M., Seth, A. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 241–252. Springer, Heidelberg (2002). doi:10.1007/3-540-36206-1_22

    Chapter  Google Scholar 

  11. Lehtinen, K.: Disjunctive form and the modal \(\mu \) alternation hierarchy. In: FICS 2015 The 10th International Workshop on Fixed Points in Computer Science, EPTCS 191, p. 117 (2015)

    Google Scholar 

  12. Lehtinen, K., Quickert, S.: Deciding the first levels of the modal mu alternation hierarchy by formula construction. In: LIPIcs-Leibniz International Proceedings in Informatics, vol. 1. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015)

    Google Scholar 

  13. Lehtinen, M.K., Quickert, S.: \(\Sigma ^{\mu }_2\) is decidable for \(\Pi ^{\mu }_2\) (extended version). Technical report. arXiv:1703.03239

  14. Lenzi, G.: A hierarchy theorem for the \(\mu \)-calculus. In: Meyer, F., Monien, B. (eds.) ICALP 1996. LNCS, vol. 1099, pp. 87–97. Springer, Heidelberg (1996). doi:10.1007/3-540-61440-0_119

    Chapter  Google Scholar 

  15. Mateescu, R.: Local model-checking of modal mu-calculus on acyclic labeled transition systems. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 281–295. Springer, Heidelberg (2002). doi:10.1007/3-540-46002-0_20

    Chapter  Google Scholar 

  16. Mostowski, A.W.: Games with forbidden sequences and finite machines. Technical report 78, Instytut Matematyki, Uniwersytet Gdański, Poland (1991)

    Google Scholar 

  17. Niwiński, D.: On fixed-point clones. In: Kott, L. (ed.) ICALP 1986. LNCS, vol. 226, pp. 464–473. Springer, Heidelberg (1986). doi:10.1007/3-540-16761-7_96

    Chapter  Google Scholar 

  18. Niwiński, D., Walukiewicz, I.: Relating hierarchies of word and tree automata. In: Morvan, M., Meinel, C., Krob, D. (eds.) STACS 1998. LNCS, vol. 1373, pp. 320–331. Springer, Heidelberg (1998). doi:10.1007/BFb0028571

    Chapter  Google Scholar 

  19. Niwiński, D., Walukiewicz, I.: A gap property of deterministic tree languages. Theor. Comput. Sci. 303(1), 215–231 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  20. Niwiński, D., Walukiewicz, I.: Deciding nondeterministic hierarchy of deterministic tree automata. Electron. Notes Theor. Comput. Sci. 123, 195–208 (2005)

    Article  MathSciNet  Google Scholar 

  21. Otto, M.: Eliminating recursion in the \(\mu \)-calculus. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, pp. 531–540. Springer, Heidelberg (1999). doi:10.1007/3-540-49116-3_50

    Chapter  Google Scholar 

  22. Rabin, M.O.: Weakly definable relations and special automata. In: Bar-Hillel, Y. (ed.) Mathematical Logic and Foundations of Set Theory, pp. 1–23 (1970)

    Google Scholar 

  23. Skrzypczak, M., Walukiewicz, I.: Deciding the topological complexity of büchi languages. In: Rabani, Y., Chatzigiannakis, I., Mitzenmacher, M., Sangiorgi, D. (eds.) 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016), vol. 55, Leibniz International Proceedings in Informatics (LIPIcs), pp. 99:1–99:13. Dagstuhl, Germany (2016). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik

    Google Scholar 

  24. Urbański, T.F.: On deciding if deterministic rabin language is in büchi class. In: Montanari, U., Rolim, J.D.P., Welzl, E. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 663–674. Springer, Heidelberg (2000). doi:10.1007/3-540-45022-X_56

    Chapter  Google Scholar 

  25. Walukiewicz, I.: Completeness of Kozen’s axiomatisation of the propositional \(\mu \)-calculus. Inf. Comput. 157(1–2), 142–182 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  26. Wilke, T.: Alternating tree automata, parity games, and modal m-calculus. Bull. Belg. Math. Soc. Simon Stevin 8(2), 359 (2001)

    MathSciNet  MATH  Google Scholar 

Download references

Achnowledgements

We thank the anonymous reviewers for their thoughtful comments and corrections. The work presented here has been supported by an EPSRC doctoral studentship at the University of Edinburgh.

Author information

Authors and Affiliations

  1. University of Kiel, Kiel, Germany

    Karoliina Lehtinen

  2. University of St. Andrews, St. Andrews, UK

    Sandra Quickert

  3. University of Edinburgh, Edinburgh, UK

    Karoliina Lehtinen & Sandra Quickert

Authors
  1. Karoliina Lehtinen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sandra Quickert
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Karoliina Lehtinen .

Editor information

Editors and Affiliations

  1. University of Turku, Turku, Finland

    Jarkko Kari

  2. Christian-Albrechts-University of Kiel, Kiel, Germany

    Florin Manea

  3. Åbo Akademi University, Turku, Finland

    Ion Petre

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Lehtinen, K., Quickert, S. (2017). \(\varSigma ^{\mu }_2\) is decidable for \(\varPi ^{\mu }_2\) . In: Kari, J., Manea, F., Petre, I. (eds) Unveiling Dynamics and Complexity. CiE 2017. Lecture Notes in Computer Science(), vol 10307. Springer, Cham. https://doi.org/10.1007/978-3-319-58741-7_28

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-58741-7_28

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-58740-0

  • Online ISBN: 978-3-319-58741-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation