390
S. Akshay et al.
transitions, s 0 ∈ S is the initial location, S f ⊆ S is a set of final locations,
n ∈ N is the number of stacks, Σ is a finite input alphabet, and Γ is a finite
stack alphabet which contains ⊥. A transition t ∈ Δ can be represented as a
tuple (s, op, a, s
), where, s, s
∈ S are respectively, the source and destination
locations of the transition t, a ∈ Σ is the label of the transition, and op is one of
the following operations (1) nop, or no stack operation, (2) (↓ i α) which pushes
α ∈ Γ onto stack i ∈ {1, 2, . . . , n}, (3) (↑ i α) which pops stack i if the top of
stack i is α ∈ Γ .
For a transition t = (s, op, a, s
) we write src(t) = s, tgt(t) = s
and op(t) =
op. At the moment we ignore the action label a but this will be useful later when
we go beyond reachability to model checking. A configuration of the MPDA is
a tuple (s, λ 1 , λ 2 , . . . , λ n ) such that, s ∈ S is the current location and λ i ∈
Γ
∗ represents the current content of i
th stack. The semantics of the MPDA
is defined as follows: a run is accepting if it starts from the initial state and
reaches a final state with all stacks empty. The language accepted by a MPDA
is defined as the set of words generated by the accepting runs of the MPDA.
Since the reachability problem for MPDA is Turing complete, we consider underapproximate reachability.
A sequence of transitions is called complete if each push in that sequence
has a matching pop and vice versa. A well-nested sequence denoted ws is
defined inductively as follows: a possibly empty sequence of nop-transitions is
ws, and so is the sequence t ws t
where op(t) = (↓ i α) and op(t
) = (↑ i α) are a
matching pair of push and pop operations of stack i, ∀i ∈ {1 . . . n}. Finally the
concatenation of two well-nested sequences is a well-nested sequence, i.e., they
are closed under concatenation. The set of all well-nested sequences defined by
an MPDA is denoted WS. If we visualize this by drawing edges between pushes
and their corresponding pops, well-nested sequences have no crossing edges, as
in
and
, where we have two stacks, depicted with red and violet
edges. We emphasize that a well-nested sequence can have well-nested edges
from any stack. In a sequence σ, a push (pop) is called a pending push (pop)
if its matching pop (push) is not in the same sequence σ.
Bounded Underapproximations. As mentioned in the introduction, different bounded under-approximations have been considered in the literature to get
around the Turing completeness of MPDA. During a computation, a context is
a sequence of transitions where only one stack or no stack is used. In context
bounded computations the number of contexts are bounded [25]. A round is a sequence of (possibly empty) contexts for stacks 1, 2, . . . , n. Round bounded computations restrict the total number of rounds allowed [19,5,6]. Scope bounded computations generalize bounded context computations. Here, the context changes
within any push and its corresponding pop is bounded [19,20,28]. A phase is a
contiguous sequence of transitions in a computation, where we restrict pop to
only one stack, but there are no restrictions on the pushes [18]. A phase bounded
computation is one where the number of phase changes is bounded.
Tree-width. A generic way of looking at them is to consider classes which
have a bound on the tree-width [22]. In fact, the notions of split-width/clique-
S. Akshay et al.
transitions, s 0 ∈ S is the initial location, S f ⊆ S is a set of final locations,
n ∈ N is the number of stacks, Σ is a finite input alphabet, and Γ is a finite
stack alphabet which contains ⊥. A transition t ∈ Δ can be represented as a
tuple (s, op, a, s
), where, s, s
∈ S are respectively, the source and destination
locations of the transition t, a ∈ Σ is the label of the transition, and op is one of
the following operations (1) nop, or no stack operation, (2) (↓ i α) which pushes
α ∈ Γ onto stack i ∈ {1, 2, . . . , n}, (3) (↑ i α) which pops stack i if the top of
stack i is α ∈ Γ .
For a transition t = (s, op, a, s
) we write src(t) = s, tgt(t) = s
and op(t) =
op. At the moment we ignore the action label a but this will be useful later when
we go beyond reachability to model checking. A configuration of the MPDA is
a tuple (s, λ 1 , λ 2 , . . . , λ n ) such that, s ∈ S is the current location and λ i ∈
Γ
∗ represents the current content of i
th stack. The semantics of the MPDA
is defined as follows: a run is accepting if it starts from the initial state and
reaches a final state with all stacks empty. The language accepted by a MPDA
is defined as the set of words generated by the accepting runs of the MPDA.
Since the reachability problem for MPDA is Turing complete, we consider underapproximate reachability.
A sequence of transitions is called complete if each push in that sequence
has a matching pop and vice versa. A well-nested sequence denoted ws is
defined inductively as follows: a possibly empty sequence of nop-transitions is
ws, and so is the sequence t ws t
where op(t) = (↓ i α) and op(t
) = (↑ i α) are a
matching pair of push and pop operations of stack i, ∀i ∈ {1 . . . n}. Finally the
concatenation of two well-nested sequences is a well-nested sequence, i.e., they
are closed under concatenation. The set of all well-nested sequences defined by
an MPDA is denoted WS. If we visualize this by drawing edges between pushes
and their corresponding pops, well-nested sequences have no crossing edges, as
in
and
, where we have two stacks, depicted with red and violet
edges. We emphasize that a well-nested sequence can have well-nested edges
from any stack. In a sequence σ, a push (pop) is called a pending push (pop)
if its matching pop (push) is not in the same sequence σ.
Bounded Underapproximations. As mentioned in the introduction, different bounded under-approximations have been considered in the literature to get
around the Turing completeness of MPDA. During a computation, a context is
a sequence of transitions where only one stack or no stack is used. In context
bounded computations the number of contexts are bounded [25]. A round is a sequence of (possibly empty) contexts for stacks 1, 2, . . . , n. Round bounded computations restrict the total number of rounds allowed [19,5,6]. Scope bounded computations generalize bounded context computations. Here, the context changes
within any push and its corresponding pop is bounded [19,20,28]. A phase is a
contiguous sequence of transitions in a computation, where we restrict pop to
only one stack, but there are no restrictions on the pushes [18]. A phase bounded
computation is one where the number of phase changes is bounded.
Tree-width. A generic way of looking at them is to consider classes which
have a bound on the tree-width [22]. In fact, the notions of split-width/clique-