Quantifier Alternation for Infinite Words
Th\'eo Pierron, Thomas Place, Marc Zeitoun

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 (sentences having at most blocks of quantifiers starting with an ) and (Boolean combinations of 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 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 and as consequences.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
Topicssemigroups and automata theory · DNA and Biological Computing · Algorithms and Data Compression
