Quantifier Alternation for Infinite Words

Abstract

We investigate the expressive power of quantifier alternation hierarchy of first-order logic over words. This hierarchy includes the classes ${\Sigma }_i$ (sentences having at most $i$ blocks of quantifiers starting with an $\exists$) and $\mathcal{B}{\Sigma }_i$ (Boolean combinations of ${\Sigma }_i$ sentences). So far, this expressive power has been effectively characterized for the lower levels only. Recently, a breakthrough was made over finite words, and decidable characterizations were obtained for $\mathcal{B}{\Sigma }_2$ and ${\Sigma }_3$, by relying on a decision problem called separation, and solving it for ${\Sigma }_2$. The contribution of this paper is a generalization of these results to the setting of infinite words: we solve separation for ${\Sigma }_2$ and ${\Sigma }_3$, and obtain decidable characterizations of $\mathcal{B}{\Sigma }_2$ and ${\Sigma }_3$ as consequences.

References in corpus (1)

• Separating regular languages by piecewise testable and unambiguous languages