Revisiting Underapproximate Reachability for Multipushdown Systems
397
decompose ρ into a finite prefix ρ 1 and an infinite suffix ρ 2 s.t. (1) both ρ 1 , ρ 2
are well-nested, or (2) ρ 1 is K-hole bounded complete (all stacks empty), and ρ 2
is well-nested, or (3) ρ 1 is K-hole bounded, and ρ 2 = (ρ 3 )
ω , where ρ 3 is K-hole
bounded. It is easy to see that (1) is solved by two calls to WellNestedReach
and choosing non-empty runs. (2) is solved by a call to Algorithm 1, modified
so that we reach s, and then calling WellNestedReach. Lastly, to solve (3), first
modify Algorithm 1 to check reachability to s with possibly non-empty stacks.
Then run the modified algorithm twice : first start from s 0 and reach s; second
start from s and reach s again.
4 Generating a Witness
We next focus on the question of generating a witness for an accepting run when
our algorithm guarantees non-emptiness. This question is important to address
from the point of view of applicability: if our goal is to see if bad states are
reachable, i.e., non-emptiness corresponds to presence of a bug, the witness run
gives the trace of how the bug came about and hence points to what can be done
to fix it (e.g., designing a controller). We remark that this question is difficult in
general. While there are naive algorithms which can explore for the witness (thus
also solving reachability), these do not use fix-point techniques and hence are
not efficient. On the other hand, since we use fix-point computations to speed
up our reachability algorithm, finding a witness, i.e., an explicit run witnessing
reachability, becomes non-trivial. Generation of a witness in the case of wellnested runs is simpler than the case when the run has holes, and requires us to
“unroll” pairs (s 0 , s f ) ∈ WR recursively and generate the sequence of transitions
responsible for (s 0 , s f ).
Getting Witnesses from Holes. Now we move on to the more complicated
case of behaviours having holes. Recall that in BFS exploration we start from
the states reachable from s 0 by well-nested sequences, and explore subsequent
states obtained either from (i) a hole creation, or (ii) a pop operation on a stack.
Proceeding in this manner, if we reach a final configuration (say s f ), with all
holes closed (which implies empty stacks), then we declare non-emptiness. To
generate a witness, we start from the final state s f reachable in the run (a leaf
node in the BFS exploration tree) and backtrack on the BFS exploration tree
till we reach the initial state s 0 . This results in generating a witness run in the
reverse, from the right to the left.
• Assume that the current node of the BFS tree was obtained using a pop
operation. There are two possibilities to consider here (see below) depending on
whether this pop operation closed or shrunk some hole. Recall that each hole
has a left end point and a right end point and is of a specific stack i, depending
on the pending pushes ↓ i it has. So, if the MPDA has k stacks, then a list in the
exploration tree can have k kinds of holes. The witness algorithm uses k stacks
called witness stacks to correctly implement the backtracking procedure, to deal
with k kinds of holes. Witness stacks should not be confused with the stacks of
the MPDA.
397
decompose ρ into a finite prefix ρ 1 and an infinite suffix ρ 2 s.t. (1) both ρ 1 , ρ 2
are well-nested, or (2) ρ 1 is K-hole bounded complete (all stacks empty), and ρ 2
is well-nested, or (3) ρ 1 is K-hole bounded, and ρ 2 = (ρ 3 )
ω , where ρ 3 is K-hole
bounded. It is easy to see that (1) is solved by two calls to WellNestedReach
and choosing non-empty runs. (2) is solved by a call to Algorithm 1, modified
so that we reach s, and then calling WellNestedReach. Lastly, to solve (3), first
modify Algorithm 1 to check reachability to s with possibly non-empty stacks.
Then run the modified algorithm twice : first start from s 0 and reach s; second
start from s and reach s again.
4 Generating a Witness
We next focus on the question of generating a witness for an accepting run when
our algorithm guarantees non-emptiness. This question is important to address
from the point of view of applicability: if our goal is to see if bad states are
reachable, i.e., non-emptiness corresponds to presence of a bug, the witness run
gives the trace of how the bug came about and hence points to what can be done
to fix it (e.g., designing a controller). We remark that this question is difficult in
general. While there are naive algorithms which can explore for the witness (thus
also solving reachability), these do not use fix-point techniques and hence are
not efficient. On the other hand, since we use fix-point computations to speed
up our reachability algorithm, finding a witness, i.e., an explicit run witnessing
reachability, becomes non-trivial. Generation of a witness in the case of wellnested runs is simpler than the case when the run has holes, and requires us to
“unroll” pairs (s 0 , s f ) ∈ WR recursively and generate the sequence of transitions
responsible for (s 0 , s f ).
Getting Witnesses from Holes. Now we move on to the more complicated
case of behaviours having holes. Recall that in BFS exploration we start from
the states reachable from s 0 by well-nested sequences, and explore subsequent
states obtained either from (i) a hole creation, or (ii) a pop operation on a stack.
Proceeding in this manner, if we reach a final configuration (say s f ), with all
holes closed (which implies empty stacks), then we declare non-emptiness. To
generate a witness, we start from the final state s f reachable in the run (a leaf
node in the BFS exploration tree) and backtrack on the BFS exploration tree
till we reach the initial state s 0 . This results in generating a witness run in the
reverse, from the right to the left.
• Assume that the current node of the BFS tree was obtained using a pop
operation. There are two possibilities to consider here (see below) depending on
whether this pop operation closed or shrunk some hole. Recall that each hole
has a left end point and a right end point and is of a specific stack i, depending
on the pending pushes ↓ i it has. So, if the MPDA has k stacks, then a list in the
exploration tree can have k kinds of holes. The witness algorithm uses k stacks
called witness stacks to correctly implement the backtracking procedure, to deal
with k kinds of holes. Witness stacks should not be confused with the stacks of
the MPDA.