394
S. Akshay et al.
Algorithm 1: Algorithm for Emptiness Checking of hole bounded
MPDA
1 Function IsEmpty(M = (S, Δ, s0, S f , n, Σ, Γ ), K):
Result: True or False
2
WR := WellNestedReach(M ); \\Solves binary reachability for pushdown system
3
if some (s0, s1) ∈ WR with s1 ∈ S f then
4
return False;
5
forall i ∈ [n] do
6
AHSi := ∅; Seti := ∅;
7
forall (s, ↓ i (α), a, s1) ∈ Δ and (s1, s
) ∈ WR do
8
AHSi := AHSi ∪ {(i, s, α, s
)}; Seti := Seti ∪ {(s, s
)};
9
HSi := {(i, s, s
) | (s, s
) ∈ TransitiveClosure(Seti)};
10
μ := [s0]; μ.NumberOfHoles := 0;
11
SetOfListsnew := {μ}; SetOfLists := ∅;
12
do
13
SetOfLists := SetOfLists ∪ SetOfListsnew;
14
SetOfLists todo := SetOfListsnew; SetOfListsnew := ∅;
15
forall μ
∈ SetOfLists todo do
16
if μ
.NumberOfHoles < K then
17
forall i ∈ [n] do
\\ Add hole for stack i
18
SetOfLists h := AddHolei(μ
, HSi) \ SetOfLists;
19
SetOfListsnew := SetOfListsnew ∪ SetOfLists h ;
20
if μ
.NumberOfHoles > 0 then
21
forall i ∈ [n] do
\\ Add pop for stack i
22
SetOfListsp := AddPopi(μ
, M, AHSi, HSi, WR) \ SetOfLists;
23
SetOfListsnew := SetOfListsnew ∪ SetOfListsp;
24
forall μ3 ∈ SetOfLists p do
25
if μ3.last ∈ S f and μ3.NumberOfHoles = 0 then
26
return False; \\If reached destination state
27
while SetOfLists new = ∅;
28
return T rue;
2. Push-Pop Closure: For stack operations, consider a push transition on
some stack (say stack i) of symbol γ, enabled from a state s 1 , reaching state
s 2 . If there is a matching pop transition from a state s 3 to s 4 , which pops
the same stack symbol γ from the stack i and if we have (s 2 , s 3 ) ∈ R c , then
we can add the tuple (s 1 , s 4 ) to R c . The function WellNestedReach repeats
this process and the transitive closure described above until a fix-point is
reached. Let us denote the resulting set of tuples by WR. Thus,
Lemma 1. (s 1 , s 2 ) ∈ WR iff ∃ a well-nested run in the MPDA from s 1 to s 2 .
Beyond well-nested reachability. A naive algorithm for K-hole bounded
reachability for K > 0 is to start from the initial state s 0 , and do a Breadth
First Search (BFS), nondeterministically choosing between extending with a
well-nested segment, creating hole segments (with a pending push) and closing
hole segments (using pops). We accept when there are no open hole segments
and reach a final state; this gives an exponential time algorithm. Given the exponential dependence on the hole-bound K (Corollary 1), this exponential blowup
is unavoidable in the worst case, but we can do much better in practice. In particular, the naive algorithm makes arbitrary non-deterministic choices resulting
in a blind exploration of the BFS tree.
S. Akshay et al.
Algorithm 1: Algorithm for Emptiness Checking of hole bounded
MPDA
1 Function IsEmpty(M = (S, Δ, s0, S f , n, Σ, Γ ), K):
Result: True or False
2
WR := WellNestedReach(M ); \\Solves binary reachability for pushdown system
3
if some (s0, s1) ∈ WR with s1 ∈ S f then
4
return False;
5
forall i ∈ [n] do
6
AHSi := ∅; Seti := ∅;
7
forall (s, ↓ i (α), a, s1) ∈ Δ and (s1, s
) ∈ WR do
8
AHSi := AHSi ∪ {(i, s, α, s
)}; Seti := Seti ∪ {(s, s
)};
9
HSi := {(i, s, s
) | (s, s
) ∈ TransitiveClosure(Seti)};
10
μ := [s0]; μ.NumberOfHoles := 0;
11
SetOfListsnew := {μ}; SetOfLists := ∅;
12
do
13
SetOfLists := SetOfLists ∪ SetOfListsnew;
14
SetOfLists todo := SetOfListsnew; SetOfListsnew := ∅;
15
forall μ
∈ SetOfLists todo do
16
if μ
.NumberOfHoles < K then
17
forall i ∈ [n] do
\\ Add hole for stack i
18
SetOfLists h := AddHolei(μ
, HSi) \ SetOfLists;
19
SetOfListsnew := SetOfListsnew ∪ SetOfLists h ;
20
if μ
.NumberOfHoles > 0 then
21
forall i ∈ [n] do
\\ Add pop for stack i
22
SetOfListsp := AddPopi(μ
, M, AHSi, HSi, WR) \ SetOfLists;
23
SetOfListsnew := SetOfListsnew ∪ SetOfListsp;
24
forall μ3 ∈ SetOfLists p do
25
if μ3.last ∈ S f and μ3.NumberOfHoles = 0 then
26
return False; \\If reached destination state
27
while SetOfLists new = ∅;
28
return T rue;
2. Push-Pop Closure: For stack operations, consider a push transition on
some stack (say stack i) of symbol γ, enabled from a state s 1 , reaching state
s 2 . If there is a matching pop transition from a state s 3 to s 4 , which pops
the same stack symbol γ from the stack i and if we have (s 2 , s 3 ) ∈ R c , then
we can add the tuple (s 1 , s 4 ) to R c . The function WellNestedReach repeats
this process and the transitive closure described above until a fix-point is
reached. Let us denote the resulting set of tuples by WR. Thus,
Lemma 1. (s 1 , s 2 ) ∈ WR iff ∃ a well-nested run in the MPDA from s 1 to s 2 .
Beyond well-nested reachability. A naive algorithm for K-hole bounded
reachability for K > 0 is to start from the initial state s 0 , and do a Breadth
First Search (BFS), nondeterministically choosing between extending with a
well-nested segment, creating hole segments (with a pending push) and closing
hole segments (using pops). We accept when there are no open hole segments
and reach a final state; this gives an exponential time algorithm. Given the exponential dependence on the hole-bound K (Corollary 1), this exponential blowup
is unavoidable in the worst case, but we can do much better in practice. In particular, the naive algorithm makes arbitrary non-deterministic choices resulting
in a blind exploration of the BFS tree.