Quantifier Alternation for Infinite Words

TL;DR

This paper extends the decidable characterization of the quantifier alternation hierarchy from finite to infinite words, solving the separation problem for levels 2 and 3, and providing new logical expressiveness results.

Contribution

It generalizes the decidable separation problem and logical class characterizations from finite to infinite words for the quantifier alternation hierarchy.

Findings

Decidable separation for ${ m extbf{ extSigma}}_2$ and ${ m extbf{ extSigma}}_3$ over infinite words.

Decidable characterizations of ${ m extbf{ extB extSigma}}_2$ and ${ m extbf{ extSigma}}_3$ over infinite words.

Extension of finite word results to the setting of 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.