# Differences

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

 expressing_finite_automata_in_msol_over_strings [2010/05/21 02:31]vkuncak expressing_finite_automata_in_msol_over_strings [2015/04/21 17:32] (current) Both sides previous revision Previous revision 2012/05/15 12:43 vkuncak 2010/05/21 02:31 vkuncak 2010/05/21 02:31 vkuncak 2009/04/29 11:09 vkuncak 2009/04/29 11:08 vkuncak 2009/04/29 11:01 vkuncak 2009/04/29 11:01 vkuncak 2009/04/29 11:01 vkuncak 2007/05/16 10:58 vkuncak 2007/05/06 21:34 vkuncak 2007/05/06 21:34 vkuncak 2007/05/06 21:25 vkuncak 2007/05/06 21:19 vkuncak 2007/05/06 21:18 vkuncak 2007/05/06 21:17 vkuncak 2007/05/06 21:16 vkuncak created Next revision Previous revision 2012/05/15 12:43 vkuncak 2010/05/21 02:31 vkuncak 2010/05/21 02:31 vkuncak 2009/04/29 11:09 vkuncak 2009/04/29 11:08 vkuncak 2009/04/29 11:01 vkuncak 2009/04/29 11:01 vkuncak 2009/04/29 11:01 vkuncak 2007/05/16 10:58 vkuncak 2007/05/06 21:34 vkuncak 2007/05/06 21:34 vkuncak 2007/05/06 21:25 vkuncak 2007/05/06 21:19 vkuncak 2007/05/06 21:18 vkuncak 2007/05/06 21:17 vkuncak 2007/05/06 21:16 vkuncak created 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 24: Line 24: Then the word is accepted if the above formula holds for the entire input Then the word is accepted if the above formula holds for the entire input - $+ \begin{equation*} ​\exists k. (F \land \forall p. k < p \rightarrow \bigwedge_i p \notin v_i) ​\exists k. (F \land \forall p. k < p \rightarrow \bigwedge_i p \notin v_i) -$ + \end{equation*}