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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
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)
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)
Dam, M.: CTL* and ECTL* as fragments of the modal μ-calculus. TCS 126(1), 77–96 (1994)
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)
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)
Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. SIAM Journal on Computing 29(1), 132–158 (2000)
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)
Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18(2), 194–211 (1979)
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)
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)
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)
Kozen, D.: Results on the propositional μ-calculus. TCS 27, 333–354 (1983)
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)
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)
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)
McNaughton, R.: Infinite games played on finite graphs. Annals of Pure and Applied Logic 65(2), 149–184 (1993)
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)
Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans.of Amer. Math.Soc. 141, 1–35 (1969)
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)
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)
Streett, R.S., Emerson, E.A.: An automata theoretic decision procedure for the propositional μ-calculus. Information and Computation 81(3), 249–264 (1989)
Walukiewicz, I.: Completeness of Kozen’s axiomatisation of the propositional μ-calculus. Inf. and Comput. 157(1–2), 142–182 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)