Differences

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

--- expressing_finite_automata_in_msol_over_strings [2007/05/06 21:34]
vkuncak
+++ expressing_finite_automata_in_msol_over_strings [2009/04/29 11:08]
vkuncak
@@ Line 16: / Line 16: @@
 \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*}
   \exists Q_0,\ldots, Q_m.\ \mbox{Init} \land (\forall p. p \leq k \rightarrow \mbox{Trans}) \land \mbox{Final}
 \end{equation*}