396
S. Akshay et al.
enough since we also need to match the stack content. Instead, we check
if we can split the hole (i, s, s
) into (1) a hole triple (i, s, s a ) ∈ HS i ,
and (2) a tuple (i, s a , α, s
) ∈ AHS i . If both (1) and (2) are possible,
then the pop transition t corresponds to the last pending push of the hole
(i, s, s
). t indeed matches the pending push recorded in the atomic hole
(i, s a , α, s
) in μ, enabling the firing of transition t from the state s k , reaching s
k . In this case, we add the child node with the list μ
obtained from
μ as follows. We replace (i) s k with s
k , and (ii) (i, s, s
) with (i, s, s a ), respectively signifying firing of the transition t and the “shrinking” of the
hole, by shifting the end point of the hole segment to the left. When we
obtain the hole triple (i, s, s) (the start and end points of the hole segment coincide), we may have uncovered the last pending push and thereby
“closed” the hole segment completely. At this point, we may choose to remove
(i, s, s) from the list, obtaining [s 0 , . . . , (h, u, v), (j, t, t
) . . . , s
k ]. For every
such μ
= [s 0 , . . . , (h, u, v), (i, s, s a ), (j, t, t
), . . . , s
k ] and all (s
k , s m ) ∈ W S
we also extend μ
to μ
= [s 0 , . . . , (h, u, v), (i, s, s a ), (j, t, t
), . . . , s m ]. Notice
that the size of the list in the child node obtained on a pop, is either the
same as the list in the parent, or is smaller.
The number of lists is bounded since the number of states and the length of
the lists are bounded. The BFS exploration tree will thus terminate. Combining
the above steps gives us Algorithm 1, whose correctness gives us:
Theorem 1. Given a MPDA and a positive integer K, Algorithm 1 terminates
and answers “false” iff there exists a K-hole bounded accepting run of the MPDA.
Complexity of the Algorithm. The maximum number of states of the system is |S|. The time complexity of transitive closure is O(|S|
3 ), using a FloydWarshall implementation. The time complexity of computing WellNestedReach
which uses the transitive closure, is O(|S|
5 ) + O(|S|
2
× (|Δ| × |S|)). To compute
AHS for n stacks the time complexity is O(n × |Δ| × |S|
2 ) and to compute HS
for n stacks the complexity is O(n×|S|
2 ). For multistack systems, each list keeps
track of (i) the number of hole segments(≤ K), and (ii) information pertaining
to holes (start, end points of holes, and which stack the hole corresponds to). In
the worst case, this will be (2K + 2) possible states in a list, as we are keeping
the states at the start and end points of all the hole segments and a stack per
hole. So, there are ≤ |S|
2K+3
× n
K+1 lists. In the worst case, when there is no
K-hole bounded run, we may end up generating all possible lists for a given
bound K on the hole segments. The time complexity is thus bounded above by
O(|S|
2K+3
× n
K+1 + |S|
5 + |S|
3
× |Δ|).
Beyond Reachability. We can solve the usual safety questions in the (boundedhole) underapproximate setting, by checking for underapproximate reachability
on the product of the given system with the complement of the safe set. Given
the way Algorithm 1 is designed, the fix-point algorithm allows us to go beyond
reachability. In particular, we can solve several (increasingly difficult) variants
of the repeated reachability problem, without much modification.
Consider the question : For a given state s and MPDA, does there exist a
run ρ starting from s 0 which visits s infinitely often? This is decidable if we can
S. Akshay et al.
enough since we also need to match the stack content. Instead, we check
if we can split the hole (i, s, s
) into (1) a hole triple (i, s, s a ) ∈ HS i ,
and (2) a tuple (i, s a , α, s
) ∈ AHS i . If both (1) and (2) are possible,
then the pop transition t corresponds to the last pending push of the hole
(i, s, s
). t indeed matches the pending push recorded in the atomic hole
(i, s a , α, s
) in μ, enabling the firing of transition t from the state s k , reaching s
k . In this case, we add the child node with the list μ
obtained from
μ as follows. We replace (i) s k with s
k , and (ii) (i, s, s
) with (i, s, s a ), respectively signifying firing of the transition t and the “shrinking” of the
hole, by shifting the end point of the hole segment to the left. When we
obtain the hole triple (i, s, s) (the start and end points of the hole segment coincide), we may have uncovered the last pending push and thereby
“closed” the hole segment completely. At this point, we may choose to remove
(i, s, s) from the list, obtaining [s 0 , . . . , (h, u, v), (j, t, t
) . . . , s
k ]. For every
such μ
= [s 0 , . . . , (h, u, v), (i, s, s a ), (j, t, t
), . . . , s
k ] and all (s
k , s m ) ∈ W S
we also extend μ
to μ
= [s 0 , . . . , (h, u, v), (i, s, s a ), (j, t, t
), . . . , s m ]. Notice
that the size of the list in the child node obtained on a pop, is either the
same as the list in the parent, or is smaller.
The number of lists is bounded since the number of states and the length of
the lists are bounded. The BFS exploration tree will thus terminate. Combining
the above steps gives us Algorithm 1, whose correctness gives us:
Theorem 1. Given a MPDA and a positive integer K, Algorithm 1 terminates
and answers “false” iff there exists a K-hole bounded accepting run of the MPDA.
Complexity of the Algorithm. The maximum number of states of the system is |S|. The time complexity of transitive closure is O(|S|
3 ), using a FloydWarshall implementation. The time complexity of computing WellNestedReach
which uses the transitive closure, is O(|S|
5 ) + O(|S|
2
× (|Δ| × |S|)). To compute
AHS for n stacks the time complexity is O(n × |Δ| × |S|
2 ) and to compute HS
for n stacks the complexity is O(n×|S|
2 ). For multistack systems, each list keeps
track of (i) the number of hole segments(≤ K), and (ii) information pertaining
to holes (start, end points of holes, and which stack the hole corresponds to). In
the worst case, this will be (2K + 2) possible states in a list, as we are keeping
the states at the start and end points of all the hole segments and a stack per
hole. So, there are ≤ |S|
2K+3
× n
K+1 lists. In the worst case, when there is no
K-hole bounded run, we may end up generating all possible lists for a given
bound K on the hole segments. The time complexity is thus bounded above by
O(|S|
2K+3
× n
K+1 + |S|
5 + |S|
3
× |Δ|).
Beyond Reachability. We can solve the usual safety questions in the (boundedhole) underapproximate setting, by checking for underapproximate reachability
on the product of the given system with the complement of the safe set. Given
the way Algorithm 1 is designed, the fix-point algorithm allows us to go beyond
reachability. In particular, we can solve several (increasingly difficult) variants
of the repeated reachability problem, without much modification.
Consider the question : For a given state s and MPDA, does there exist a
run ρ starting from s 0 which visits s infinitely often? This is decidable if we can