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 [2009/04/29 11:01] vkuncak |
expressing_finite_automata_in_msol_over_strings [2010/05/21 02:31] vkuncak |
||
---|---|---|---|
Line 2: | Line 2: | ||
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$. | ||
+ | |||
+ | 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 | 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 | ||
Line 16: | 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*} | ||
- | Note: we need to take care of the end of the string as well, by introducing the set of all positions in the input string, often denoted $\$$. | + | 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) | ||
+ | \] |