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 ,
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.
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.
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 .
This follows from closure properties of finite state machines, take automata that denote union and complement of the languages.
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.
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.
- Cosmological Lower Bound on the Circuit Complexity of a Small Problem in Logic (See the introduction and the conclusion sections)
- circuit versus assymptotic time complexity (uniformity, specific instance versus assymptotic bound)
- the density question
- do we need to know how to check validity for all MSOL formulas