Differences

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

--- reachable_pushdown_configurations_are_regular [2007/05/30 23:02]
vkuncak
+++ reachable_pushdown_configurations_are_regular [2007/05/31 00:09]
vkuncak
@@ Line 9: / Line 9: @@
   * $\Gamma$ is a finite stack alphabet
   * $\Delta \subseteq (P \times \Gamma) \times (P \times \Gamma^*)$ is a set of transition rules
-This is like a pushdown automaton, but there are no input symbols, and there are no final states.  This is because we are interested in reachable states, not the language accepted by the automaton.
+This is like a pushdown automaton, but there are no input symbols, and there are no final states.  This is because we are interested in reachable states, not the language accepted by the automaton.  If $((q,\gamma),(q',w)$, we write $(q,\gamma) \leadsto (q',w)$.  Intuitively, this condition means that when the topmost stack symbol is $\gamma$ and the automaton is in the state $q$, the automaton can transition to a new state $q'$ and replace the symbol $\gamma$ with the string $w$.  Note that, as a special case, if $w$ is an empty string, the automaton does a pop, and if the string is of the form $\alpha \gamma$, then it pushes $\alpha$ on top of the stack.
+The configuration of a pushdown system is given by a pair $(q,w)$ where $q \in P$ and $w \in \Gamma^*$.  The transition relation on configurations is given by relation
+\begin{equation*}
+ r = \{ ((q,\gamma w'),(q',w w') \mid ((q,\gamma),(q',w) \in \Delta \}
+\end{equation*}
+In an application to verification, this relation represents the meaning of the program.  We are therefore interested in propagating error states backwards from some set of states to determine all initial states that could lead to an error.
+=== Multi-automata ===
+We represent the sets of reachable states as an automaton.  Let $P = \{ p^1,\ldots,p^m\}$.  We represent a set $T$ of pushdown configurations, which are elements of $P \times \Gamma^*$, by splitting it according to $P$, so that $T = \cup_i \{(p^i,w) \mid w \in L^i\}$.  Therefore, $L^i \subseteq \Gamma^*$ represents the set of possible values for stacks when the automaton is in the state $p^i$.  We define each $L^i$ as the language accepted by a finite state machine.  It turns out that we can use the same set of states for machines representing different $L^i$, all we need to introduce are different initial states.  This leads to the notion of multi-automaton, which is just an ordinary non-deterministic [[finite state machine]], but with a //set// of initial states instead of just one initial state.  Specifically, we define a multi-automaton for the pushdown system with control states $P$ as ${\cal A} = (\Gamma,Q,\delta,I,F)$ where the input alphabet $\Gamma$ for the finite state machine is the stack alphabet of the pushdown system, $Q$ is some finite set of states of the multi-automaton, $\delta \subseteq Q \times \Gamma \times Q$, $F \subseteq Q$.  The set $I = \{ s^1,\ldots,s^m \}$ of initial states has one initial state for each control state of the pushdown system.
+=== Computing pre-image of a regular set ===
+Given a set of $T \subseteq P \times \Gamma^*$ of pushdown system configurations, its pre-image is the set
+\begin{equation*}
+  \mbox{pre}(T) = \{ (p^j,\gamma w') \mid ((p^j, \gamma),(p^k,w)) \in \Delta\ \land\ (p^k,w w') \in T \}
+\end{equation*}
+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 \}
+\end{equation*}