Revisiting Underapproximate Reachability for Multipushdown Systems
391
width/tree-width of communicating finite state machines/timed push down systems has been explored in [3], [13]. The behaviors of the underlying system are
then represented as graphs. It has been shown in these references that if the family of graphs arising from the behaviours of the underlying system (say S) have
a bounded tree-width, then the reachability problem is decidable for S via, treeautomata. However, this does not immediately give rise to an efficient implementation. The tree-automata approach usually gives non-deterministic or bottomup tree automata, which when implemented in practice (see [6]) tend to blow up
in size and explore a large and useless space. Hence there is a need for efficient
algorithms, which exist for more specific underapproximations such as contextbounded (leading to fix-point algorithms and their implementations [21]).
2.1
A new class of under-approximations
Our goal is to bridge the gap between having practically efficient algorithms
and handling more expressive classes of under-approximations for reachability
of multi-stack pushdown systems. To do so, we define a bounded approximation
which is expressive enough to cover previously defined practically interesting
classes (such as context bounded etc), while at the same time allowing efficient
decidable reachability tests, as we will see in the next section.
Definition 1. (Holes). Let σ be complete sequence of transitions, of length n in
a MPDA, and let ws be a well-nested sequence.
– A hole of stack i is a maximal factor of σ of the form (↓ i ws)
+ , where
ws ∈ WS. The maximality of the hole of stack i follows from the fact that
any possible extension ceases to be a hole of stack i; that is, the only possible
events following a maximal hole of stack i are a push ↓ j of some stack j = i,
or a pop of some stack j = i. In general, whenever we speak about a hole,
the underlying stack is clear.
– A push ↓ i in a hole (of stack i) is called a pending push at (i.e., just before)
a position x ≤ n, if its matching pop occurs in σ at a position z > x.
– A hole (of stack i) is said to be open at a position x ≤ n, if there is a
pending push ↓ i of the hole at x. Let # x (hole) denote the number of open
holes at position x. The hole bound of σ is defined as max 1≤x≤|σ| # x (hole).
– 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.
As an example, consider the sequence σ in Figure 1 of transitions of a MPDA
having stacks 1,2 (denoted respectively red and blue). We use superscripts for
s0
ws1
↓
1
1 ↓
2
1
↓
3
1
ws2
ws3
ws4
↓
1
2 ↓
2
2
↑
3
1 ↑
2
1
ws5
↓
4
1 ↓
5
1 ↑
2
2 ↑
5
1 ↑
1
2 ↑
4
1 ↑
1
1
sf
↓
1
1 ↓
2
1
↓
3
1
↓
1
2 ↓
2
2
↓
4
1 ↓
5
1
Figure 1. A run σ with 2 holes (2 red patches) of the red stack and 1 hole (one blue
patch) of the blue stack.
391
width/tree-width of communicating finite state machines/timed push down systems has been explored in [3], [13]. The behaviors of the underlying system are
then represented as graphs. It has been shown in these references that if the family of graphs arising from the behaviours of the underlying system (say S) have
a bounded tree-width, then the reachability problem is decidable for S via, treeautomata. However, this does not immediately give rise to an efficient implementation. The tree-automata approach usually gives non-deterministic or bottomup tree automata, which when implemented in practice (see [6]) tend to blow up
in size and explore a large and useless space. Hence there is a need for efficient
algorithms, which exist for more specific underapproximations such as contextbounded (leading to fix-point algorithms and their implementations [21]).
2.1
A new class of under-approximations
Our goal is to bridge the gap between having practically efficient algorithms
and handling more expressive classes of under-approximations for reachability
of multi-stack pushdown systems. To do so, we define a bounded approximation
which is expressive enough to cover previously defined practically interesting
classes (such as context bounded etc), while at the same time allowing efficient
decidable reachability tests, as we will see in the next section.
Definition 1. (Holes). Let σ be complete sequence of transitions, of length n in
a MPDA, and let ws be a well-nested sequence.
– A hole of stack i is a maximal factor of σ of the form (↓ i ws)
+ , where
ws ∈ WS. The maximality of the hole of stack i follows from the fact that
any possible extension ceases to be a hole of stack i; that is, the only possible
events following a maximal hole of stack i are a push ↓ j of some stack j = i,
or a pop of some stack j = i. In general, whenever we speak about a hole,
the underlying stack is clear.
– A push ↓ i in a hole (of stack i) is called a pending push at (i.e., just before)
a position x ≤ n, if its matching pop occurs in σ at a position z > x.
– A hole (of stack i) is said to be open at a position x ≤ n, if there is a
pending push ↓ i of the hole at x. Let # x (hole) denote the number of open
holes at position x. The hole bound of σ is defined as max 1≤x≤|σ| # x (hole).
– 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.
As an example, consider the sequence σ in Figure 1 of transitions of a MPDA
having stacks 1,2 (denoted respectively red and blue). We use superscripts for
s0
ws1
↓
1
1 ↓
2
1
↓
3
1
ws2
ws3
ws4
↓
1
2 ↓
2
2
↑
3
1 ↑
2
1
ws5
↓
4
1 ↓
5
1 ↑
2
2 ↑
5
1 ↑
1
2 ↑
4
1 ↑
1
1
sf
↓
1
1 ↓
2
1
↓
3
1
↓
1
2 ↓
2
2
↓
4
1 ↓
5
1
Figure 1. A run σ with 2 holes (2 red patches) of the red stack and 1 hole (one blue
patch) of the blue stack.