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:34] vkuncak |
expressing_finite_automata_in_msol_over_strings [2009/04/29 11:01] vkuncak |
||
---|---|---|---|
Line 16: | Line 16: | ||
\end{equation*} | \end{equation*} | ||
- | To express 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 |
\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 \$. |