On the variable hierarchy of the modal μ-calculus

Abstract

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.