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 (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.
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}
}