This is an old revision of the document!

Expressing finite automaton in MSOL over strings

Consider a finite automaton with alphabet $\Sigma=\{0,1\}^n$ , states $Q = \{q_0,q_1,\ldots,q_m\}$ , transition relation $\Delta$ , initial state $q_0$ and final states $F$ .

There exists an execution of an automaton iff there exist the intermediate states given by transition relation $\Delta$ . We describe intermediate states using sets $Q_0,\ldots,Q_m$ , one for each state of the in $Q$ . The state $Q_i$ is the set of positions in the execution at which the automaton is in state $q_i$ . We encode the transition relation $\Delta$ using the formula

$\begin{equation*} \mbox{Tran} = \bigwedge (p+1) \in Q_v \leftrightarrow \bigvee_{(q_v,(a_1,\ldots,a_n),q_w) \in \Delta} (p \in Q_w \land \bigwedge_{i=1}^n (p \in v_i)^{a_{ij}}) \end{equation*}$