Disjunctive form and the modal μ alternation hierarchy

Karoliina Lehtinen

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.

In Ralph Matthes and Matteo Mio: Proceedings Tenth International Workshop on Fixed Points in Computer Science (FICS 2015), Berlin, Germany, September 11-12, 2015, Electronic Proceedings in Theoretical Computer Science 191, pp. 117–131.
Published: 9th September 2015.

ArXived at: http://dx.doi.org/10.4204/EPTCS.191.11 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org