Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

sav08:projection_of_automata [2009/04/17 14:00]
vkuncak
sav08:projection_of_automata [2015/04/21 17:30] (current)
Line 4: Line 4:
  
 Given a language $L \subseteq \Sigma^*$, define Given a language $L \subseteq \Sigma^*$, define
-\[+\begin{equation*}
    ​proj(x,​L) =     ​proj(x,​L) = 
 \begin{array}[t]{@{}l} \begin{array}[t]{@{}l}
 \{ a_1 \ldots a_n \mid \exists b_1,​\ldots,​b_n \in \{0,1\}. a_1[x:=b_1] \ldots a_n[x:=b_n] \in L \} \\ \{ a_1 \ldots a_n \mid \exists b_1,​\ldots,​b_n \in \{0,1\}. a_1[x:=b_1] \ldots a_n[x:=b_n] \in L \} \\
-\{ a_1[x:=b_1] \ldots a_n[x:=b_n] \mid b_1,​\ldots,​b_n \in \{0,1\}a_1 \ldots a_n \in L \}+\{ a_1[x:=b_1] \ldots a_n[x:=b_n] \mid b_1,​\ldots,​b_n \in \{0,1\}, \ a_1 \ldots a_n \in L \}
 \end{array} \end{array}
-\]+\end{equation*}
  
 Given a [[:Finite state machine|finite automaton]] $A = (\Sigma,​Q,​\Delta,​q_0,​F)$,​ define projection $proj(x,A)$ as $(\Sigma,​Q,​\Delta',​q_0,​F)$ where Given a [[:Finite state machine|finite automaton]] $A = (\Sigma,​Q,​\Delta,​q_0,​F)$,​ define projection $proj(x,A)$ as $(\Sigma,​Q,​\Delta',​q_0,​F)$ where
-\[+\begin{equation*}
     \Delta'​ = \{(q,​a,​q'​) \mid \exists b \in \{0,1\}. (q,​a[x:​=b],​q'​) \in \Delta \}     \Delta'​ = \{(q,​a,​q'​) \mid \exists b \in \{0,1\}. (q,​a[x:​=b],​q'​) \in \Delta \}
-\]+\end{equation*}
  
 **Lemma:** $L(proj(x,​A)) = proj(x,​L(A))$ **Lemma:** $L(proj(x,​A)) = proj(x,​L(A))$
  
 Given a regular expression $r$, define $proj(x,r)$ by Given a regular expression $r$, define $proj(x,r)$ by
-\[+\begin{equation*}
 \begin{array}{l} \begin{array}{l}
 proj(x,[F]) = [qe(\exists x.F)] \\ proj(x,[F]) = [qe(\exists x.F)] \\
Line 27: Line 27:
 proj(x,r_1 + r_2) = proj(x,r_1) + proj(x,r_2) proj(x,r_1 + r_2) = proj(x,r_1) + proj(x,r_2)
 \end{array} \end{array}
-\]+\end{equation*}
  
 **Lemma:** $L(proj(x,​r)) = proj(x,​L(r))$ **Lemma:** $L(proj(x,​r)) = proj(x,​L(r))$
  
 
sav08/projection_of_automata.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice