Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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)
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*}
  
 
expressing_finite_automata_in_msol_over_strings.txt · Last modified: 2015/04/21 17:32 (external edit)