Disjunctive form and the modal $\mu$ alternation hierarchy

TL;DR

This paper investigates the relationship between disjunctive form and the modal mu calculus's alternation hierarchy, revealing that disjunctive form does not preserve alternation depth and highlighting complexities in hierarchy decision problems.

Contribution

It demonstrates that disjunctive formulas do not preserve alternation depth under tableau equivalence, providing new insights into the complexity of the alternation hierarchy.

Findings

Disjunctive formulas with high alternation depth can be tableau equivalent to alternation-free formulas.

Non-disjunctive formulas of high alternation depth can be tableau equivalent to disjunctive formulas without alternations.

Disjunctive form does not preserve alternation depth, impacting understanding of hierarchy complexity.

Abstract

This paper studies the relationship between disjunctive form, a syntactic normal form for the modal mu calculus, and the alternation hierarchy. First it shows that all disjunctive formulas which have equivalent tableau have the same syntactic alternation depth. However, tableau equivalence only preserves alternation depth for the disjunctive fragment: there are disjunctive formulas with arbitrarily high alternation depth that are tableau equivalent to alternation-free non-disjunctive formulas. Conversely, there are non-disjunctive formulas of arbitrarily high alternation depth that are tableau equivalent to disjunctive formulas without alternations. This answers negatively the so far open question of whether disjunctive form preserves alternation depth. The classes of formulas studied here illustrate a previously undocumented type of avoidable syntactic complexity which may contribute to our understanding of why deciding the alternation hierarchy is still an open problem.