Quantifier alternation for infinite words

Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Complexity of computation (including implicit computational complexity) (03D15)

Abstract: We investigate the expressive power of quantifier alternation hierarchy of first-order logic over words. This hierarchy includes the classes

{S i g m a}_{i}

(sentences having at most

i

blocks of quantifiers starting with an

e x i s t s

) and

m a t h c a l B {S i g m a}_{i}

(Boolean combinations of

{S i g m a}_{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

m a t h c a l B {S i g m a}_{2}

and

{S i g m a}_{3}

, by relying on a decision problem called separation, and solving it for

{S i g m a}_{2}

. The contribution of this paper is a generalization of these results to the setting of infinite words: we solve separation for

{S i g m a}_{2}

and

{S i g m a}_{3}

, and obtain decidable characterizations of

m a t h c a l B {S i g m a}_{2}

and

{S i g m a}_{3}

as consequences.

Recommendations

Cites work

Cited in

(13)

This page was built for publication: Quantifier alternation for infinite words

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2811342)