Abstract
We give a complete axiomatization for the modal μ-calculus on finite trees. While the completeness of our axiomatization already follows from a more powerful result by Igor Walukiewicz in [11], our proof is easier and uses very different tools, inspired from model theory. We show that our approach generalizes to certain axiomatic extensions, and to the extension of the μ-calculus with graded modalities. We hope that the method might be helpful for other completeness proofs as well.
Chapter PDF
Similar content being viewed by others
References
Bojańczyk, M.: Effective characterizations of tree logics. In: PODS 2008: Proceedings of the twenty-seventh ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, pp. 53–66. ACM, New York (2008)
Demri, S., Lugiez, D.: Presburger modal logic is only PSPACE-complete. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 541–556. Springer, Heidelberg (2006)
Doets, K.: Monadic \(\Pi_1^1\)-theories of \(\Pi_1^1\)-properties. Notre Dame Journal of Formal Logic 30(2) (1989)
Fattorosi-Barnaba, M., Cerrato, C.: Graded modalities I. Studia Logica, 47 (1988)
Fischer, M., Ladner, R.: Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18(2) (1979)
Gheerbrant, A., ten Cate, B.: Complete axiomatizations of MSO, FO(TC1) and FO(LFP1) on finite trees. In: LFCS (2009)
Kozen, D.: Results on the propositional μ-calculus. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, Springer, Heidelberg (1995)
Libkin, L.: Logics for unranked trees: An overview. Logical Methods in Computer Science 2(3) (2006)
de Rijke, M., Blackburn, P., Venema, Y.: Modal Logic. Cambridge University Press (1991)
ten Cate, B.: Model theory for extended modal languages. PhD thesis, University of Amsterdam, ILLC Dissertation Series DS-2005-01 (2005)
Walukiewicz, I.: A note on the completeness of Kozen’s axiomatization of the propositional μ-calculus. The Bulletin of Symbolic Logic 2(3) (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
ten Cate, B., Fontaine, G. (2010). An Easy Completeness Proof for the Modal μ-Calculus on Finite Trees. In: Ong, L. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2010. Lecture Notes in Computer Science, vol 6014. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12032-9_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-12032-9_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12031-2
Online ISBN: 978-3-642-12032-9
eBook Packages: Computer ScienceComputer Science (R0)