×

The variable hierarchy of the \(\mu\)-calculus is strict. (English) Zbl 1121.68072

Summary: Most of the logics commonly used in verification, such as LTL, CTL, \(\text{CTL}^{*}\), and PDL can be embedded into the two-variable fragment of the \(\mu\)-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 \(\mu\)-formulae can be bounded in general. We answer this question negatively and prove that the variable-hierarchy of the \(\mu\)-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 \(\mu\)-calculus, thus resolving an open issue raised by Parikh in 1983.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
03B45 Modal logic (including the logic of norms)
Full Text: DOI