LARA

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 $G$ and for all $k$, for 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_{21},\ldots,a_{n1}) ... (a_{1k},a_{2k},\ldots,a_{nk}) \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.

NOTE: What if the witness is longer than $k$?

  • concatenate the language of strings of the form $[\bigwedge_{j=1,j\neq i}^n \lnot v_j]*$ to the language of the automaton
  • there exists $k_0$ so that equivalence holds for all $k \ge k_0$

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.

References