Revisiting Underapproximate Reachability for Multipushdown Systems
395
In this section, we use the binary well-nested reachability algorithm as an
efficient subroutine to limit the search in BFS to its reachable part (note that
this is quite different from DFS as well since we do not just go down one path).
The crux is that at any point, we create a new hole for stack i, only when (i)
we know that we cannot reach the final state without creating this hole and (ii)
we know that we can close all such holes which have been created. Checking (i)
is easy, since we just use the WR relation for this. Checking (ii) blindly would
correspond to doing a DFS; however, we precompute this information and simply
look it up, resulting in a constant time operation after the precomputation.
Precomputing hole information. Recall that a hole of stack i is a maximal
sequence of the form (↓ i ws)
+ , where ws is a well-nested sequence and ↓ i represents a push of stack i. A hole segment of stack i is a prefix of a hole of stack
i, ending in a ws, while an atomic hole segment of stack i is just the segment
of the form ↓ i ws. A hole-segment of stack i which starts from state s in the
MPDA and ends in state s
, can be represented by the triple (i, s, s
), that we
call a hole triple. We compute the set HS i of all hole triples (i, s, s
) such that
starting at s, there is a hole segment of stack i which ends at state s
, as detailed
in lines (5-9) of Algorithm 1. In doing so, we also compute the set AHS i of all
atomic hole segments of stack i and store them as tuples of the form (i, s p , α, s q )
such that s p and s q are the MPDA states respectively at the left and right end
points of an atomic hole segment of stack i, and α is the symbol pushed on stack
i (s p
↓i(α)ws
− −−−− → s q ).
A guided BFS exploration. We start with a list μ 0 = [s 0 ] consisting of
the initial state and construct a BFS exploration tree whose nodes are lists of
bounded length. A list is a sequence of states and hole triples representing a
K-hole bounded run in a concise form. If H i represents a hole triple for stack i,
then a list is a sequence of the form [s, H i , H j , H k , H i , . . . , H , s
]. The simplest
kind of list is a single state s. For example, a list with 3 holes of stacks i, j, k is
μ = [s 0 ,(i, s, s
),(j, r, r
),(k, t, t
),t
]. The hole triples (in red) denote open holes
in the list. The maximum number of open holes in a list is bounded, making the
length of the list also bounded. Let last(μ) represent the last element of the list
μ. This is always a state. For a node v storing list μ in the BFS tree, if v 1 , . . . v k
are its children, then the corresponding lists μ 1 , . . . μ k are obtained by extending
the list μ by one of the following operations:
1. Extend μ with a hole. Assume there is a hole of some stack i, which starts
at last(μ) = s, and ends at s
. If the list at the parent node v is μ = [. . . , s],
then for all (i, s, s
) ∈ HS i , we obtain the list trunc(μ) · append[(i, s, s
), s
] at
the child node (i.e., we remove the last element s of μ, then append to this
list the hole triple (i, s, s
), followed by s
).
2. Extend μ with a pop. Suppose there is a transition t = (s k , ↑ i (α), a, s
k )
from last(μ) = s k , where μ is of the form [s0, . . . , (h, u, v), (i, s, s
), (j, t, t
) . . . , s k ],
such that there is no hole triple of stack i after (i, s, s
), we extend the run
by matching this pop (with its push). However, to obtain the last pending push of stack i corresponding to this hole, just HS i information is not
395
In this section, we use the binary well-nested reachability algorithm as an
efficient subroutine to limit the search in BFS to its reachable part (note that
this is quite different from DFS as well since we do not just go down one path).
The crux is that at any point, we create a new hole for stack i, only when (i)
we know that we cannot reach the final state without creating this hole and (ii)
we know that we can close all such holes which have been created. Checking (i)
is easy, since we just use the WR relation for this. Checking (ii) blindly would
correspond to doing a DFS; however, we precompute this information and simply
look it up, resulting in a constant time operation after the precomputation.
Precomputing hole information. Recall that a hole of stack i is a maximal
sequence of the form (↓ i ws)
+ , where ws is a well-nested sequence and ↓ i represents a push of stack i. A hole segment of stack i is a prefix of a hole of stack
i, ending in a ws, while an atomic hole segment of stack i is just the segment
of the form ↓ i ws. A hole-segment of stack i which starts from state s in the
MPDA and ends in state s
, can be represented by the triple (i, s, s
), that we
call a hole triple. We compute the set HS i of all hole triples (i, s, s
) such that
starting at s, there is a hole segment of stack i which ends at state s
, as detailed
in lines (5-9) of Algorithm 1. In doing so, we also compute the set AHS i of all
atomic hole segments of stack i and store them as tuples of the form (i, s p , α, s q )
such that s p and s q are the MPDA states respectively at the left and right end
points of an atomic hole segment of stack i, and α is the symbol pushed on stack
i (s p
↓i(α)ws
− −−−− → s q ).
A guided BFS exploration. We start with a list μ 0 = [s 0 ] consisting of
the initial state and construct a BFS exploration tree whose nodes are lists of
bounded length. A list is a sequence of states and hole triples representing a
K-hole bounded run in a concise form. If H i represents a hole triple for stack i,
then a list is a sequence of the form [s, H i , H j , H k , H i , . . . , H , s
]. The simplest
kind of list is a single state s. For example, a list with 3 holes of stacks i, j, k is
μ = [s 0 ,(i, s, s
),(j, r, r
),(k, t, t
),t
]. The hole triples (in red) denote open holes
in the list. The maximum number of open holes in a list is bounded, making the
length of the list also bounded. Let last(μ) represent the last element of the list
μ. This is always a state. For a node v storing list μ in the BFS tree, if v 1 , . . . v k
are its children, then the corresponding lists μ 1 , . . . μ k are obtained by extending
the list μ by one of the following operations:
1. Extend μ with a hole. Assume there is a hole of some stack i, which starts
at last(μ) = s, and ends at s
. If the list at the parent node v is μ = [. . . , s],
then for all (i, s, s
) ∈ HS i , we obtain the list trunc(μ) · append[(i, s, s
), s
] at
the child node (i.e., we remove the last element s of μ, then append to this
list the hole triple (i, s, s
), followed by s
).
2. Extend μ with a pop. Suppose there is a transition t = (s k , ↑ i (α), a, s
k )
from last(μ) = s k , where μ is of the form [s0, . . . , (h, u, v), (i, s, s
), (j, t, t
) . . . , s k ],
such that there is no hole triple of stack i after (i, s, s
), we extend the run
by matching this pop (with its push). However, to obtain the last pending push of stack i corresponding to this hole, just HS i information is not