Mu-depth 3 is more than 2: A game-theoretic proof (Q2719798)

The paper addresses a specific expressiveness problem in the propositional modal mu-calculus, introduced by \textit{D. Kozen} [``Results on the propositional mu-calculus'', Theor. Comput. Sci. 27, 333-354 (1983; Zbl 0553.03007)]. The `mu' means that it is a logic capable of expressing least and greatest solutions of fixed point equations \(X=f(X)\) denoted, respectively, \(\mu X. f(X)\) and \(\nu X. f(X)\). The mu-calculus formulas can be classified according to their fixed point alternation depth, i.e., the number of non-trivial nestings of alternating least and greatest fixed points: Properties such as safety and liveness have to be expressed with at least one alternation formulas, whereas two alternations are required to express fairness. For a long time no property was known to require three or more alternations, but \textit{J. C. Bradfield} [``The modal mu-calculus alternation hierarchy is strict'', Theor. Comput. Sci. 195, 133-153 (1998; Zbl 0915.03017)] proved that such formulas exist, and that the fixed point alternation (f.a.d.) hierarchy is infinite. A particular case of Bradfield's result is proved, in the sense that an explicit formula is given that lies in the third level of the hierarchy. Some semantical properties of f.a.d. 2 formulas are used to find mu-calculus properties not expressible by any f.a.d. 2 formula, and a new kind of game on infinite trees is introduced for studying the complexity of expressing a particular f.a.d. 2 formula (the `infinitely often P' formula).