Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
expressing_finite_automata_in_msol_over_strings [2007/05/06 21:25] vkuncak |
expressing_finite_automata_in_msol_over_strings [2009/04/29 11:08] vkuncak |
||
---|---|---|---|
Line 7: | Line 7: | ||
\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 \} | \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*} | \end{equation*} | ||
- | Initially, the autonaton is in the initial state: | + | Initially, the automaton is in the initial state: |
\begin{equation*} | \begin{equation*} | ||
\mbox{Init} = 0 \in Q_0 \land \bigwedge_{u=1}^m (0 \notin Q_u) | \mbox{Init} = 0 \in Q_0 \land \bigwedge_{u=1}^m (0 \notin Q_u) | ||
\end{equation*} | \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 | ||
+ | \begin{equation*} | ||
+ | \exists Q_0,\ldots, Q_m.\ \mbox{Init} \land (\forall p. p \leq k \rightarrow \mbox{Trans}) \land \mbox{Final} | ||
+ | \end{equation*} | ||
+ | |||