Abstract
The modal μ-calculus L μ attains high expressive power by extending basic modal logic with monadic variables and binding them to extremal fixed points of definable operators. The number of variables occurring in a formula provides a relevant measure of its conceptual complexity. In a previous paper with Erich Grädel we have shown, for the existential fragment of L μ , that this conceptual complexity is also reflected in an increase of semantic complexity, by providing examples of existential formulae with k variables that are not equivalent to any existential formula with fewer than k variables.
In this paper, we prove an existential preservation theorem for the family of L μ -formulae over at most k variables that define simulation closures of finite strongly connected structures. Since hard formulae for the level k of the existential hierarchy belong to this family, it follows that the bounded variable fragments of the full modal μ-calculus form a hierarchy of strictly increasing expressive power.
This research has been partially supported by the European Community Research Training Network “Games and Automata for Synthesis and Validation” (games).
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
Arnold, A.: The mu-calculus alternation-depth is strict on binary trees. RAIRO Informatique Théorique et Applications 33, 329–339 (1999)
Arnold, A., Niwiński, D.: Rudiments of μ-calculus. North Holland, Amsterdam (2001)
Berwanger, D.: Game logic is strong enough for parity games. Studia Logica 75, 205–219 (2003); Special issue on Game Logic and Game Algebra edited by Pauly M., Parikh, R.
Berwanger, D., Grädel, E.: Games and model checking for guarded logics. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 70–84. Springer, Heidelberg (2001)
Berwanger, D., Grädel, E., Lenzi, G.: On the variable hierarchy of the modal mgr-calculus. In: Bradfield, J. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, pp. 352–366. Springer, Heidelberg (2002)
Berwanger, D., Lenzi, G.: Robbers, guardians, and a few diamonds. Hard patterns in the μ-calculus variable hierarchy (submitted)
Bradfield, J.: The modal μ-calculus alternation hierarchy is strict. Theoretical Computer Science 195, 133–153 (1998)
d’Agostino, G., Hollenberg, M.: Logical questions concerning the μ-calculus: interpolation, Lyndon, and Łos-Tarski. Journal of Symbolic Logic 65, 310–332 (2000)
Emerson, A., Jutla, C.: Tree automata, mu-calculus and determinacy. In: Proc. 32nd IEEE Symp. on Foundations of Computer Science, pp. 368–377 (1991)
Hennessy, M.C.B., Milner, R.: On observing nondeterminism and concurrency. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85. Springer, Heidelberg (1980)
Janin, D., Lenzi, G.: On the logical definability of topologically closed recognizable languages of infinite trees. Computing and Informatics 21, 185–203 (2002)
Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)
Kozen, D.: A finite model theorem for the propositional μ-calculus. Studia Logica 47, 233–241 (1988)
Kupferman, O., Vardi, M., Wolper, P.: An automata-theoretic approach to branching-time model checking. Journal of the ACM 47, 312–360 (2000)
Lenzi, G.: A hierarchy theorem for the mu-calculus. In: Meyer auf der Heide, F., Monien, B. (eds.) ICALP 1996. LNCS, vol. 1099, pp. 87–97. Springer, Heidelberg (1996)
Parikh, R.: The logic of games and its applications. Annals of Discrete Mathematics 24, 111–140 (1985)
Pauly, M.: Logic for Social Software, PhD thesis, University of Amsterdam (2001)
Stirling, C.: Bisimulation, modal logic and model checking games. Logic Journal of the IGPL 7, 103–124 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berwanger, D., Lenzi, G. (2005). The Variable Hierarchy of the μ-Calculus Is Strict. In: Diekert, V., Durand, B. (eds) STACS 2005. STACS 2005. Lecture Notes in Computer Science, vol 3404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31856-9_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-31856-9_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-24998-6
Online ISBN: 978-3-540-31856-9
eBook Packages: Computer ScienceComputer Science (R0)