We investigate the structure of the modal μ-calculus
L
μ
with respect to the question of how many different fixed point variables are necessary to define a given property. Most of
the logics commonly used in verification, such as CTL, LTL, CTL
*, PDL, etc. can in fact be embedded into the two-variable fragment of the μ-calculus. It is also known that the two-variable
fragment can express properties that occur at arbitrarily high levels of the alternation hierarchy. However, it is an open
problem whether the variable hierarchy is strict.
Here we study this problem with a game-based approach and establish the strictness of the hierarchy for the case of existential
(i.e.,□-free) formulae. It is known that these characterize precisely the Lμ-definable properties that are closed under extensions. We also relate the strictness of the variable hierarchy to the question
whether the finite variable fragments satisfy the existential preservation theorem.