Revisiting Underapproximate Reachability for Multipushdown Systems
393
N}. A possible word w ∈ L
bh is a
3 b
3 a
2 c
3 b
2 d
3 a
2 c
3 bd
2 ac
2 bd
2 with a, b representing push in stack 1,2 respectively and c, d representing the corresponding
matching pop from stack 1,2. A run ρ accepting the word w ∈ L
bh will start
with a sequence of pushes of stack 1 followed by another sequence of pushes of
stack 2. Note that, the number of the pushes n is same in both stacks. Then
there is a group G consisting of a well-nested sequence of stack 1 (equal a and
c) followed by a pop of the stack 1 (an extra c), another well-nested sequence
of stack 2 (equal b and d) and a pop of the stack 2 (an extra d), repeated n
times. From the definition of the hole, the total number of holes required in G
is 0. But, we need 1 hole for the sequence of a’s and another for the sequence
of b’s at the beginning of the run, which creates at most 2 holes during the run.
Thus, the hole bound for any accepting run ρ is 2, and the language L
bh is 2-hole
bounded.
However, L
bh is not k-scope bounded for any k. Indeed, for each m ≥ 1,
consider the word w m = a
m b
m (ac
2 bd
2 )
m
∈ L
bh . It is easy to see that w m is 2mscope bounded (the matching c, d of each a, b happens 2m context switches later)
but not k-scope bounded for k < 2m. It can be seen that L
bh is not k-phase
bounded either. Finally, L
= {(ab)
n c
n d
n
| n ∈ N} with a, b and c, d respectively
being push and pop of stack 1,2 is not hole-bounded but 2-phase bounded.
3 A Fix-point Algorithm for Hole Bounded Reachability
In the previous section, we showed that hole-bounded underapproximations are
a decidable subclass for reachability, by showing that this class has a bounded
tree-width. However, as explained in the introduction, this does not immediately
give a fix-point based algorithm, which has been shown to be much more efficient for other more restricted sub-classes, e.g., context-bounded. In this section,
we provide such a fix-point based algorithm for the hole-bounded class and explain its advantages. Later we discuss its versatility by showing extensions and
evaluating its performance on a suite of benchmarks.
We describe the algorithm in two steps: first we give a simple fix-point based
algorithm for the problem of 0-hole or well-nested reachability, i.e, reachability by
a well-nested sequence without any holes. For the 0-hole case, our algorithm computes the reachability relation, also called the binary reachability problem [15].
That is, we accept all pairs of states (s, s
) such that there is a well-nested run
from s with empty stack to s
with empty stack. Subsequently, we combine this
binary reachability for well-nested sequences with an efficient graph search to
obtain an algorithm for K-hole bounded reachability.
Binary well-nested reachability for MPDA. Note that single stack PDA are
a special case, since all runs are indeed well-nested.
1. Transitive Closure: Let R be the set of tuples of the form (s i , s j ) representing that state s j is reachable from state s i via a nop discrete transition. Such
a sequence from s i to s j is trivially well-nested. We take the TransitiveClosure
of R using Floyd-Warshall algorithm [12]. The resulting set R c of tuples answers the binary reachability for finite state automata (no stacks).
393
N}. A possible word w ∈ L
bh is a
3 b
3 a
2 c
3 b
2 d
3 a
2 c
3 bd
2 ac
2 bd
2 with a, b representing push in stack 1,2 respectively and c, d representing the corresponding
matching pop from stack 1,2. A run ρ accepting the word w ∈ L
bh will start
with a sequence of pushes of stack 1 followed by another sequence of pushes of
stack 2. Note that, the number of the pushes n is same in both stacks. Then
there is a group G consisting of a well-nested sequence of stack 1 (equal a and
c) followed by a pop of the stack 1 (an extra c), another well-nested sequence
of stack 2 (equal b and d) and a pop of the stack 2 (an extra d), repeated n
times. From the definition of the hole, the total number of holes required in G
is 0. But, we need 1 hole for the sequence of a’s and another for the sequence
of b’s at the beginning of the run, which creates at most 2 holes during the run.
Thus, the hole bound for any accepting run ρ is 2, and the language L
bh is 2-hole
bounded.
However, L
bh is not k-scope bounded for any k. Indeed, for each m ≥ 1,
consider the word w m = a
m b
m (ac
2 bd
2 )
m
∈ L
bh . It is easy to see that w m is 2mscope bounded (the matching c, d of each a, b happens 2m context switches later)
but not k-scope bounded for k < 2m. It can be seen that L
bh is not k-phase
bounded either. Finally, L
= {(ab)
n c
n d
n
| n ∈ N} with a, b and c, d respectively
being push and pop of stack 1,2 is not hole-bounded but 2-phase bounded.
3 A Fix-point Algorithm for Hole Bounded Reachability
In the previous section, we showed that hole-bounded underapproximations are
a decidable subclass for reachability, by showing that this class has a bounded
tree-width. However, as explained in the introduction, this does not immediately
give a fix-point based algorithm, which has been shown to be much more efficient for other more restricted sub-classes, e.g., context-bounded. In this section,
we provide such a fix-point based algorithm for the hole-bounded class and explain its advantages. Later we discuss its versatility by showing extensions and
evaluating its performance on a suite of benchmarks.
We describe the algorithm in two steps: first we give a simple fix-point based
algorithm for the problem of 0-hole or well-nested reachability, i.e, reachability by
a well-nested sequence without any holes. For the 0-hole case, our algorithm computes the reachability relation, also called the binary reachability problem [15].
That is, we accept all pairs of states (s, s
) such that there is a well-nested run
from s with empty stack to s
with empty stack. Subsequently, we combine this
binary reachability for well-nested sequences with an efficient graph search to
obtain an algorithm for K-hole bounded reachability.
Binary well-nested reachability for MPDA. Note that single stack PDA are
a special case, since all runs are indeed well-nested.
1. Transitive Closure: Let R be the set of tuples of the form (s i , s j ) representing that state s j is reachable from state s i via a nop discrete transition. Such
a sequence from s i to s j is trivially well-nested. We take the TransitiveClosure
of R using Floyd-Warshall algorithm [12]. The resulting set R c of tuples answers the binary reachability for finite state automata (no stacks).