The variable hierarchy for the games -calculus

Parity games are combinatorial representations of closed Boolean μ -terms. By adding to them draw positions, they have been organized by Arnold and Santocanale (2005, 2007) [3,27] into a μ -calculus (Arnold, 2001 [2]) whose standard interpretation is over the class of all complete lattices. As done by Berwanger et al. (2002, 2005) [8,9] for the propositional modal μ -calculus, it is possible to classify parity games into levels of a hierarchy according to the number of fixed-point variables. We ask whether this hierarchy collapses w.r.t. the standard interpretation. We answer this question negatively by providing, for each n ≥ 1 , a parity game G n with these properties: it unravels to a μ -term built up with n fixed-point variables, it is not semantically equivalent to any game with strictly less than n − 2 fixed-point variables.