English

Quantifier Alternation for Infinite Words

Formal Languages and Automata Theory 2015-12-01 v1

Abstract

We investigate the expressive power of quantifier alternation hierarchy of first-order logic over words. This hierarchy includes the classes Σi{\Sigma}_i (sentences having at most ii blocks of quantifiers starting with an \exists) and BΣi\mathcal{B}{\Sigma}_i (Boolean combinations of Σi{\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 BΣ2\mathcal{B}{\Sigma}_2 and Σ3{\Sigma}_3, by relying on a decision problem called separation, and solving it for Σ2{\Sigma}_2. The contribution of this paper is a generalization of these results to the setting of infinite words: we solve separation for Σ2{\Sigma}_2 and Σ3{\Sigma}_3, and obtain decidable characterizations of BΣ2\mathcal{B}{\Sigma}_2 and Σ3{\Sigma}_3 as consequences.

Keywords

Cite

@article{arxiv.1511.09011,
  title  = {Quantifier Alternation for Infinite Words},
  author = {Théo Pierron and Thomas Place and Marc Zeitoun},
  journal= {arXiv preprint arXiv:1511.09011},
  year   = {2015}
}
R2 v1 2026-06-22T11:56:31.371Z