This is an old revision of the document!

Reachable pushdown configurations are regular

We next show that in a push down system, the pre-image of a regular set of configurations is again a regular set of configurations. Moreover, the new finite state machine for configurations can use the same set of states as the original one. This gives an algorithm for verifying regular properties of push down automata by representing them using finite state machines. Based on the introductory part of Reachability Analysis of Pushdown Automata: Application to Model Checking.

Pushdown system

A pushdown system is a triple ${\cal P} = (P, \Gamma, \Delta)$ where

$P$ is a finite set of states, called control locations
$\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. 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.