Deciding FO2 Alternation for Automata over Finite and Infinite Words

We consider two-variable first-order logic $\text{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 $\mathbf{NL}$. In particular, this leads to $\mathbf{NL}$ algorithms for deciding the levels of the $\text{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 $\mathbf{NL}$-hard and, hence, $\mathbf{NL}$-complete.