Differences

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

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