388
S. Akshay et al.
multi-pushdown systems while remaining efficiently implementable. Our algorithm works for a new class of underapproximate behaviors called hole bounded
behaviors, which subsumes context/scope bounded underapproximations, and
is orthogonal to phase bounded underapproximations. A “hole” is a maximal
sequence of push operations of a fixed stack, interspersed with well-nested sequences of any stack. Thus, in a sequence α = βγ where β = [push 1 (push 2 push 3
pop 3 pop 2 )push 1 (push 3 pop 3 )]
10 and γ = push2push1pop2pop1(pop1)
20 , β is a hole
with respect to stack 1. The suffix γ has 2 holes (the push 2 and the push 1 ).
Thus we say that α is 3-hole bounded. On the other hand, the number of context switches (and scope bound) in α is > 50. A (k-)hole bounded sequence is one
such, where, at any point of the computation, the number of “open” holes are
bounded at this point (by k). We show that the class of hole bounded sequences
subsumes most of the previously defined classes of underapproximations and is,
in fact, contained in the very generic class of tree-width bounded sequences. This
immediately shows decidability of the reachability problem for our class.
Analyzing the more generic class of tree-width bounded sequences is often
much more difficult; for instance, building bottom-up tree automata for this
purpose does not scale very well as it explores a large (and often useless) state
space. Our technique is radically different from using tree automata. Under the
hole bounded assumption, we pre-compute information regarding well-nested
sequences and holes using fix-point computations and use them in our algorithm.
Using efficient data structures to implement this approach, we develop a tool
(BHIM) for Bounded Hole reachability in Multi-stack pushdown systems.
Highlights of BHIM.
• Two significant aspects of the fix-point approach in BHIM are: (i) we efficiently
solve the binary reachability problem for pushdown automata. i.e., BHIM computes all pairs of states (s, t) such that t is reachable from s with empty stacks.
This allows us to go beyond reachability and handle some liveness questions; (ii)
we pre-compute the set of pairs of states that are endpoints of holes. This allows
us to greatly limit the search for an accepting run.
• While the fix-point approach solves (binary) reachability efficiently, it does not
a priori produce a witness of reachability. We remedy this situation by proposing
a backtracking algorithm, which cleverly uses the computations done in the fixpoint algorithm, to generate a witness efficiently.
• BHIM is parametrized with respect to the hole bound: if non-emptiness can
be checked or witnessed by a well-nested sequence (this is an easy witness and
BHIM looks for easy witnesses first, then gradually increases complexity, if no
easy witness is found), then it is sufficient to have the hole bound 0. Increasing
this complexity measure as required to certify non-emptiness gives an efficient
implementation, in the sense that we search for harder witnesses only when no
easier witnesses (w.r.t this complexity measure) exist. In examples described in
the experimental section, a small (less than 4) bound suffices and we expect this
to be the case for most practical examples.
• Finally, we extend our approach to handle timed multi-stack pushdown systems. This shows the versatility of our approach and also requires us to solve
S. Akshay et al.
multi-pushdown systems while remaining efficiently implementable. Our algorithm works for a new class of underapproximate behaviors called hole bounded
behaviors, which subsumes context/scope bounded underapproximations, and
is orthogonal to phase bounded underapproximations. A “hole” is a maximal
sequence of push operations of a fixed stack, interspersed with well-nested sequences of any stack. Thus, in a sequence α = βγ where β = [push 1 (push 2 push 3
pop 3 pop 2 )push 1 (push 3 pop 3 )]
10 and γ = push2push1pop2pop1(pop1)
20 , β is a hole
with respect to stack 1. The suffix γ has 2 holes (the push 2 and the push 1 ).
Thus we say that α is 3-hole bounded. On the other hand, the number of context switches (and scope bound) in α is > 50. A (k-)hole bounded sequence is one
such, where, at any point of the computation, the number of “open” holes are
bounded at this point (by k). We show that the class of hole bounded sequences
subsumes most of the previously defined classes of underapproximations and is,
in fact, contained in the very generic class of tree-width bounded sequences. This
immediately shows decidability of the reachability problem for our class.
Analyzing the more generic class of tree-width bounded sequences is often
much more difficult; for instance, building bottom-up tree automata for this
purpose does not scale very well as it explores a large (and often useless) state
space. Our technique is radically different from using tree automata. Under the
hole bounded assumption, we pre-compute information regarding well-nested
sequences and holes using fix-point computations and use them in our algorithm.
Using efficient data structures to implement this approach, we develop a tool
(BHIM) for Bounded Hole reachability in Multi-stack pushdown systems.
Highlights of BHIM.
• Two significant aspects of the fix-point approach in BHIM are: (i) we efficiently
solve the binary reachability problem for pushdown automata. i.e., BHIM computes all pairs of states (s, t) such that t is reachable from s with empty stacks.
This allows us to go beyond reachability and handle some liveness questions; (ii)
we pre-compute the set of pairs of states that are endpoints of holes. This allows
us to greatly limit the search for an accepting run.
• While the fix-point approach solves (binary) reachability efficiently, it does not
a priori produce a witness of reachability. We remedy this situation by proposing
a backtracking algorithm, which cleverly uses the computations done in the fixpoint algorithm, to generate a witness efficiently.
• BHIM is parametrized with respect to the hole bound: if non-emptiness can
be checked or witnessed by a well-nested sequence (this is an easy witness and
BHIM looks for easy witnesses first, then gradually increases complexity, if no
easy witness is found), then it is sufficient to have the hole bound 0. Increasing
this complexity measure as required to certify non-emptiness gives an efficient
implementation, in the sense that we search for harder witnesses only when no
easier witnesses (w.r.t this complexity measure) exist. In examples described in
the experimental section, a small (less than 4) bound suffices and we expect this
to be the case for most practical examples.
• Finally, we extend our approach to handle timed multi-stack pushdown systems. This shows the versatility of our approach and also requires us to solve