Differences

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

--- reachable_pushdown_configurations_are_regular [2007/05/31 00:09]
vkuncak
+++ reachable_pushdown_configurations_are_regular [2007/05/31 00:22]
vkuncak
@@ Line 30: / Line 30: @@
 which contains all states that can lead to a state in $T$.  Given the representation of $T$ using a family of sets $L^i$, we can define the corresponding pre-image computation of $L^i$ by
 \begin{equation*}
-  \mbox{pre}(L^j) = \{ \gamma w' \mid ((p^j, \gamma),(p^k,w w')) \in \Delta\ \land\ w w' \in L^k \}
+  \mbox{pre}(L^j) = \{ \gamma w' \mid ((p^j, \gamma),(p^k,w)) \in \Delta\ \land\ w w' \in L^k \}
 \end{equation*}
+To translate this operation into operations on automata, a word $\gamma w'$ should be accepted starting from state $p^j$ whenever the word $ww'$ is accepted starting from state $p^k$.  We can ensure this by introducing tuples $(p^j,\gamma,q)$ for all states $q$ that the automaton could be in after reading a word $w$ starting from the state $p^k$.  We need to do this for all transitions $((p^j, \gamma),(p^k,w)) \in \Delta$.
+=== Fixpoint computation ===
+To reach the set of all states that can result in a state in $T$ in zero or one steps, we compute $T \cup \mbox{pre}(T)$ by keeping the previous edges along with the new ones in the multi-automaton.  By repeating this process we obtain the exact representation of the set of states that can reach states in the original regular set of configurations.  This process converges because we only add new edges, never add new states to the automaton, so the maximal number of edges is bounded.