LARA

This is an old revision of the document!

Using automata to decide MSOL over strings

Compare this to Using automata to decide Presburger arithmetic.

We will define $A(G)$ such that for every $k$ and every matrix $a_{ij} \in \{0,1\}$ where for $1 \leq i \leq n$ and $1 \leq j \leq k$,

\begin{equation*} [\![G]\!] [v_i \mapsto \{j \mid a_{ij}=1 \}]_{i=1}^n = \mbox{true} \end{equation*}

iff

\begin{equation*} (a_{11},a_{12},\ldots,a_{1n}) ... (a_{k1},a_{k2},\ldots,a_{kn}) \in L(A(G)) \end{equation*} 

a11 ... a1k         --->   v1
a21 ... a2k         --->   v2
... ... ...         ...
an1 ... ank         --->   vn

 ^
 |
L(G)

In matrix $a_{ij}$, row $i$ gives the set for variable $v_i$, whereas column $j$ gives the $j$-th symbol of the input word for the automaton.

Case $A(v_i \subseteq v_j)$

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

Case $A(s(v_p,v_q))$

The automaton expects to see first a sequence of symbols $(a_1,\ldots,a_k)$ such that $a_p=0, a_q=0$, then a symbol with $a_p=1, a_q=0$ followed by a symbol with $a_p=0, a_q=1$, followed again by a sequence with $a_p=0, a_q=0$.

Case $A(G_1 \lor G_2)$, $A(\lnot G)$

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

Case $A(\exists v_i. G)$

This is projection operation on an automaton. Take $A(G)$ and replace each transition with label $(a_1,\ldots,a_i,\ldots,a_n)$ with two transitions $(a_1,\ldots,0,\ldots,a_n)$ and $(a_1,\ldots,1,\ldots,a_n)$ into the same destination state.

This is because existentially quantifying over an integer is the same as existentially quantifying over all of its bits.

As in the case of Presbuger arithmetic, to check if $F$ is satisfiable, we construct $A(F)$ as a deterministic automaton and check whether the graph of $A(F)$ 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 $\exists$ and $\forall$ we obtain an exponential blowup. For formula with n alternations we have $2^{2^{\ldots 2}}$ complexity with a stack of exponentials of height $n$. 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.