Quantifier Alternation for Infinite Words

2015/11/29 by Pierron, Théo, Place, Thomas, Zeitoun, Marc
#FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL)

paper · doi:10.48550/arxiv.1511.09011

Abstract

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

Related

• Going higher in the First-order Quantifier Alternation Hierarchy on Words
• Going Higher in First-Order Quantifier Alternation Hierarchies on Words
• Level Two of the Quantifier Alternation Hierarchy over Infinite Words
• Nesting negations in FO2 over infinite words
• Decidability, Complexity, and Expressiveness of First-Order Logic Over the Subword Ordering