Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
expressing_finite_automata_in_msol_over_strings [2009/04/29 11:09] vkuncak |
expressing_finite_automata_in_msol_over_strings [2012/05/15 12:43] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Expressing finite automaton in MSOL over strings ====== | + | ====== Expressing finite automaton in WS1S ====== |
| 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$. | 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$. | ||
| Line 18: | Line 18: | ||
| \end{equation*} | \end{equation*} | ||
| - | To express the property that an automaton accepts a string whose length is given by free variable $k$ we then use formula | + | 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*} | \begin{equation*} | ||
| \exists Q_0,\ldots, Q_m.\ \mbox{Init} \land (\forall p. p \leq k \rightarrow \mbox{Trans}) \land \mbox{Final} | \exists Q_0,\ldots, Q_m.\ \mbox{Init} \land (\forall p. p \leq k \rightarrow \mbox{Trans}) \land \mbox{Final} | ||
| \end{equation*} | \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) | ||
| + | \] | ||