# Using automata to decide MSOL over strings

Compare this to Using automata to decide Presburger arithmetic.

We will define such that for every and for all , for every matrix where for and , iff a11 ... a1k         --->   v1
a21 ... a2k         --->   v2
... ... ...         ...
an1 ... ank         --->   vn

^
|
L(G)

In matrix , row gives the set for variable , whereas column gives the -th symbol of the input word for the automaton.

Case The automaton checks that every input symbol is suchj that if then also . If it ever encounters a different symbol, it goes into an error state.

Case The automaton expects to see first a sequence of symbols such that , then a symbol with followed by a symbol with , followed again by a sequence with .

Case , This follows from closure properties of finite state machines, take automata that denote union and complement of the languages.

Case This is projection operation on an automaton. Take and replace each transition with label with two transitions and into the same destination state. This is because existentially quantifying over an integer is the same as existentially quantifying over all of its bits.

NOTE: What if the witness is longer than ?

• concatenate the language of strings of the form to the language of the automaton
• there exists so that equivalence holds for all As in the case of Presbuger arithmetic, to check if is satisfiable, we construct as a deterministic automaton and check whether the graph of has a reachable accepting state.

## Complexity

The above construction determinizes automaton whenever it needs to perform negation. Moreover, existential quantifier forces the automaton to be non-deterministic. Therefore, with every alternation between and we obtain an exponential blowup. For formula with n alternations we have complexity with a stack of exponentials of height . Is there a better algorithm? The following paper shows that, in the worst case such behavior cannot be avoided, because of such high expressive power of MSOL over strings.