LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

expressing_finite_automata_in_msol_over_strings [2010/05/21 02:31]
vkuncak 		expressing_finite_automata_in_msol_over_strings [2015/04/21 17:32]
Line 1: Line 1:
-====== 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$. 
- 
-Let the sets $v_i$ denote the encoding of input string of the automaton. 
- 
-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_w \leftrightarrow \bigvee \{ (p \in Q_u \land \bigwedge_{i=1}^n (p \in v_i)^{a_{ij}}) \mid (q_u,​(a_1,​\ldots,​a_n),​q_w) \in \Delta \} 
-\end{equation*} 
-Initially, the automaton is in the initial state: 
-\begin{equation*} 
-  \mbox{Init} = 0 \in Q_0 \land \bigwedge_{u=1}^m (0 \notin Q_u) 
-\end{equation*} 
-and at some final position $k$ it should be in final state: 
-\begin{equation*} 
-  \mbox{Final} = \bigvee_{u=0}^m (k \in Q_u) 
-\end{equation*} 
- 
-To express the property that an automaton accepts a string whose length is given by free variable $k$ we then use formula $F$: 
-\begin{equation*} 
-  \exists Q_0,\ldots, Q_m.\ \mbox{Init} \land (\forall p. p \leq k \rightarrow \mbox{Trans}) \land \mbox{Final} 
-\end{equation*} 
- 
-Then the word is accepted if the above formula holds for the entire input 
-\[ 
-   ​\exists k. (F \land \forall p. k < p \rightarrow \bigwedge_i p \notin v_i) 
-\]