The variable hierarchy of the $mu$-calculus is strict.

Abstract. Most of the logics commonly used in verification, such as LTL, CTL, CTL∗, and PDL can be embedded into the two-variable fragment of the µ-calculus. It is also known that properties occurring at arbitrarily high levels of the alternation hierarchy can be formalised using only two variables. This raises the question of whether the number of fixed-point variables in µ-formulae can be bounded in general. We answer this question negatively and prove that the variable-hierarchy of the µ-calculus is semantically strict. For any k, we provide examples of formulae with k variables that are not equivalent to any formula with fewer variables. In particular, this implies that Parikh’s Game Logic is less expressive than the µ-calculus, thus resolving an open issue raised by Parikh in 1983.