Skip to main content
SpringerLink
Log in

The Modal μ-Calculus Caught Off Guard

  • Conference paper
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2011)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 6793))

Abstract

The modal μ-calculus extends basic modal logic with second-order quantification in terms of arbitrarily nested fixpoint operators. Its satisfiability problem is EXPTIME-complete. Decision procedures for the modal μ-calculus are not easy to obtain though since the arbitrary nesting of fixpoint constructs requires some combinatorial arguments for showing the well-foundedness of least fixpoint unfoldings. The tableau-based decision procedures so far also make assumptions on the unfoldings of fixpoint formulas, e.g. explicitly require formulas to be in guarded normal form. In this paper we present a tableau calculus for deciding satisfiability of arbitrary, i.e. not necessarily guarded μ-calculus formulas. The novel contribution is a new unfolding rule for greatest fixpoint formulas which shows how to handle unguardedness without an explicit transformation into guarded form, thus avoiding a (seemingly) exponential blow-up in formula size. We prove soundness and completeness of the calculus, and discuss its advantages over existing approaches.

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

Access this chapter

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 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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Banieqbal, B., Barringer, H.: Temporal logic with fixed points. In: Banieqbal, B., Pnueli, A., Barringer, H. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 62–73. Springer, Heidelberg (1989)

    Chapter  Google Scholar 

  2. Bradfield, J., Stirling, C.: Modal logics and μ-calculi: an introduction. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra. Elsevier, Amsterdam (2001)

    Google Scholar 

  3. Dam, M.: CTL* and ECTL* as fragments of the modal μ-calculus. TCS 126(1), 77–96 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  4. Emerson, E.A.: Automata, tableaux and temporal logics. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 79–87. Springer, Heidelberg (1985)

    Chapter  Google Scholar 

  5. Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Models and Semantics, vol. B, ch. 16, pp. 996–1072. Elsevier and MIT Press, New York, USA (1990)

    Google Scholar 

  6. Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. SIAM Journal on Computing 29(1), 132–158 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  7. Emerson, E.A., Lei, C.L.: Efficient model checking in fragments of the propositional μ–calculus. In: Symposion on Logic in Computer Science, pp. 267–278. IEEE, Washington, D.C. (1986)

    Google Scholar 

  8. Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18(2), 194–211 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  9. Friedmann, O., Lange, M.: A solver for modal fixpoint logics. In: Proc. 6th Workshop on Methods for Modalities, M4M-6. Elect. Notes in Theor. Comp. Sc., vol. 262, pp. 99–111 (2010)

    Google Scholar 

  10. Janin, D., Walukiewicz, I.: On the expressive completeness of the propositional μ-calculus with respect to monadic second order logic. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 263–277. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  11. Jungteerapanich, N.: A tableau system for the modal μ-calculus. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 220–234. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  12. Kozen, D.: Results on the propositional μ-calculus. TCS 27, 333–354 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  13. Kozen, D., Parikh, R.: A decision procedure for the propositional μ-calculus. In: Clarke, E., Kozen, D. (eds.) Logic of Programs 1983. LNCS, vol. 164, pp. 313–325. Springer, Heidelberg (1984)

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  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)

    Chapter  Google Scholar 

  16. McNaughton, R.: Infinite games played on finite graphs. Annals of Pure and Applied Logic 65(2), 149–184 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  17. Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. In: Proc. 21st Symp.on Logic in Computer Science (LICS 2006), pp. 255–264. IEEE Computer Society, Los Alamitos (2006)

    Google Scholar 

  18. Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans.of Amer. Math.Soc. 141, 1–35 (1969)

    MathSciNet  MATH  Google Scholar 

  19. Schewe, S.: Solving parity games in big steps. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 449–460. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  20. Streett, R.S., Emerson, E.A.: The propositional μ-calculus is elementary. In: Paredaens, J. (ed.) ICALP 1984. LNCS, vol. 172, pp. 465–472. Springer, Heidelberg (1984)

    Chapter  Google Scholar 

  21. Streett, R.S., Emerson, E.A.: An automata theoretic decision procedure for the propositional μ-calculus. Information and Computation 81(3), 249–264 (1989)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computer Science, University of Munich, Germany

    Oliver Friedmann

  2. Dept. of Elect. Eng. and Computer Science, University of Kassel, Germany

    Martin Lange

Authors
  1. Oliver Friedmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Lange
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Informatik und Angewandte Mathematik, Universität Bern, Neubrückstr. 10, 3012, Bern, Switzerland

    Kai Brünnler

  2. Mathematisches Institut, Universität Bern, Sidlerstr. 5, 3012, Bern, Switzerland

    George Metcalfe

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Friedmann, O., Lange, M. (2011). The Modal μ-Calculus Caught Off Guard. In: Brünnler, K., Metcalfe, G. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2011. Lecture Notes in Computer Science(), vol 6793. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22119-4_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-22119-4_13

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-22118-7

  • Online ISBN: 978-3-642-22119-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation