The modal mu index problem

The modal $\mu$ calculus, which consists of modal logic with fixpoint operators, is an expressive specification logic with palatable decidability properties: satisfiability is EXPTIME and the model-checking problem—which is equivalent to solving a parity game—is quasi-polynomial, conjectured to be in P. The $\mu$ calculus is essentially a logical formalism describing alternating parity automata on node-labelled trees with arbitrary, unordered branching.

My thesis, entitles “Syntactic Complexity in the Modal $\mu$ Calculus” is about recognising syntactic complexity from semantic complexity—that is, recognising when formulas can be simplified. This is a well-known problem known as both the Alternation Hierarchy and the Parity, Mostowski or Rabin–Mostowski Index Problem. The question is whether, given a formula of the $\mu$ calculus, the existence of an equivalent formula with a fixed number of alternations between greatest and least fixpoints is decidable.

One of the more interesting contribution of my thesis is a characterisation of formulas of any complexity that are equivalent to $\mu\nu$ formulas, that is, formulas that describe co-Büchi languages (and, dually, Büchi languages, as everything is dualisable). This characterisation gives, for any formula, a parameterised co-Büchi formula that is equivalent to the original formula, for some large enough parameter, if and only if the original formula is equivalent to some co-Büchi formula. You will find this in Chapter 6 of my thesis linked below, and Theorem 93 is the key result. The technique is a little different from Thomas Colcombet and Christof Löding’s reduction to distance-parity automata, as the target formula is alternating rather than non-deterministic. A further difference is that Colcombet and Löding’s result is for automata that operate on trees with a fixed number of ordered successors; I am not sure whether the same method works for $\mu$ formulas or parity automata on unrestricted trees, since the crutial notion of guidable automata does not seem to generalise easily.

In Chapter 5 you will also find a very simple procedure to turn $\mu$ formulas into equivalent safety/co-safety formulas, that is formulas with just one type of fixpoint operator, if they exist.