This is an old revision of the document!
Backward reachable pushdown configurations are regular
Example:
- program with procedures that ensures proper use of a global lock
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 where
is a finite set of states, called control locations
is a finite stack alphabet
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 , we write
. Intuitively, this condition means that when the topmost stack symbol is
and the automaton is in the state
, the automaton can transition to a new state
and replace the symbol
with the string
. Note that, as a special case, if
is an empty string, the automaton does a pop, and if the string is of the form
, then it pushes
on top of the stack.
The configuration of a pushdown system is given by a pair where
and
. The transition relation on configurations is given by relation
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 . We represent a set
of pushdown configurations, which are elements of
, by splitting it according to
, so that
. Therefore,
represents the set of possible values for stacks when the automaton is in the state
. We define each
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
, 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
as
where the input alphabet
for the finite state machine is the stack alphabet of the pushdown system,
is some finite set of states of the multi-automaton,
,
. The set
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 of pushdown system configurations, its pre-image is the set
which contains all states that can lead to a state in . Given the representation of
using a family of sets
, we can define the corresponding pre-image computation of
by
To translate this operation into operations on automata, a word should be accepted starting from state
whenever the word
is accepted starting from state
. We can ensure this by introducing tuples
for all states
that the automaton could be in after reading a word
starting from the state
. We need to do this for all transitions
.
Fixpoint computation
To reach the set of all states that can result in a state in in zero or one steps, we compute
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.