Deciding FO2 Alternation for Automata over Finite and Infinite Words
share
We consider two-variable first-order logic FO^2 and its quantifier alternation hierarchies over both finite and infinite words. Our main results are forbidden patterns for deterministic automata (finite words) and for Carton-Michel automata (infinite words). In order to give concise patterns, we allow the use of subwords on paths in finite graphs. This concept is formalized as subword patterns. Deciding the presence or absence of such a pattern in a given automaton is in 𝐍𝐋. In particular, this leads to 𝐍𝐋 algorithms for deciding the levels of the FO^2 quantifier alternation hierarchies. This applies to both full and half levels, each over finite and infinite words. Moreover, we show that these problems are 𝐍𝐋-hard and, hence, 𝐍𝐋-complete.
READ FULL TEXT