Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
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)
 
© EPFL 2018 - Legal notice