Revisiting Underapproximate Reachability for Multipushdown Systems
399
some of the significant challenges and advances, leaving the formal details and
algorithms to the supplement [4]. A TMPDA extends a MPDA S with a set X
of clock variables. Transitions check constraints which are conjunctions/disjunctions of constraints (called closed guards in the literature) of the form x ≤ c or
x ≥ c for c ∈ N and x any clock from X . Symbols pushed on stacks “age” with
time elapse; that os, they store the time elapsed since they were pushed onto the
stack. A pop is successful only when the age of the symbol lies within a certain
interval. The acceptance condition is as in the case of MPDA.
The first main challenge in adapting the algorithms in section 3 to the timed
setting was to take care of all possible time elapses along with the operations
defined in Algorithm 1. The usage of closed guards in TMPDA means that it suffices to explore all runs with integral time elapses (for a proof see e.g., Lemma 4.1
in [5]). Thus configurations are pairs of states with valuations that are vectors of
non-negative integers, each of which is bounded by the maximal constant in the
system. Now, to check reachability we need to extend all the precomputations
(transitive closure, well-nested reachability, as well as atomic and non-atomic
hole segments) with the time elapse information. To do this, we use a weighted
version of the Floyd-Warshall algorithm by storing time elapses during precomputations. This allows us to use this precomputed timed well-nested reachability
information while performing the BFS tree exploration, thus ensuring that any
explored state is indeed reachable by a timed run. In doing so, the most challenging part is extending the BFS tree wrt a pop. Here, we not only have to find a
split of a hole into an atomic hole-segment and a hole-segment as in Algorithm 1,
but also need to keep track of possible partitions of time, making the algorithm
quite challenging.
Timed Witness: As in the untimed case, we generate a witness certifying nonemptiness of TMPDA. But, producing a witness for the fix-point computation
as discussed earlier requires unrolling. The fix-point computation generates a
pre-computed set WRT of tuples ((s, ν), t, (s
, ν
)), where s, s
are states t is time
elapsed in the well-nested sequence and ν, ν
∈ N
|X | are integral valuations, i.e.,
integer values taken by clocks. This set of tuples does not have information
about the intermediate transitions and time-elapses. To handle this, using the
pre-computed information, we define a lexicographic progress measure which
ensures termination of this search. The main idea is as follows: the first progress
measure is to check if there a time-elapse t transition possible between (s, ν) and
(s
, ν
) and if so, we print this out. If not, ν
= ν + t, and some set of clocks
have been reset in the transition(s) from (s, ν) to (s
, ν
). The second progress
measure looks at the sequence of transitions from (s, ν) to (s
, ν
), consisting of
reset transitions (at most the number of clocks) that result in ν
from ν. If neither
the first nor the second progress measure apply, then ν = ν
, and we are left to
explore the last progress measure, by exploring at most |S| number of transitions
from (s, ν) to (s
, ν
). Using this progress measure, we can seamlessly extend the
witness generation to the timed setting. The challenges involved therein, can be
seen in the full version [4].
399
some of the significant challenges and advances, leaving the formal details and
algorithms to the supplement [4]. A TMPDA extends a MPDA S with a set X
of clock variables. Transitions check constraints which are conjunctions/disjunctions of constraints (called closed guards in the literature) of the form x ≤ c or
x ≥ c for c ∈ N and x any clock from X . Symbols pushed on stacks “age” with
time elapse; that os, they store the time elapsed since they were pushed onto the
stack. A pop is successful only when the age of the symbol lies within a certain
interval. The acceptance condition is as in the case of MPDA.
The first main challenge in adapting the algorithms in section 3 to the timed
setting was to take care of all possible time elapses along with the operations
defined in Algorithm 1. The usage of closed guards in TMPDA means that it suffices to explore all runs with integral time elapses (for a proof see e.g., Lemma 4.1
in [5]). Thus configurations are pairs of states with valuations that are vectors of
non-negative integers, each of which is bounded by the maximal constant in the
system. Now, to check reachability we need to extend all the precomputations
(transitive closure, well-nested reachability, as well as atomic and non-atomic
hole segments) with the time elapse information. To do this, we use a weighted
version of the Floyd-Warshall algorithm by storing time elapses during precomputations. This allows us to use this precomputed timed well-nested reachability
information while performing the BFS tree exploration, thus ensuring that any
explored state is indeed reachable by a timed run. In doing so, the most challenging part is extending the BFS tree wrt a pop. Here, we not only have to find a
split of a hole into an atomic hole-segment and a hole-segment as in Algorithm 1,
but also need to keep track of possible partitions of time, making the algorithm
quite challenging.
Timed Witness: As in the untimed case, we generate a witness certifying nonemptiness of TMPDA. But, producing a witness for the fix-point computation
as discussed earlier requires unrolling. The fix-point computation generates a
pre-computed set WRT of tuples ((s, ν), t, (s
, ν
)), where s, s
are states t is time
elapsed in the well-nested sequence and ν, ν
∈ N
|X | are integral valuations, i.e.,
integer values taken by clocks. This set of tuples does not have information
about the intermediate transitions and time-elapses. To handle this, using the
pre-computed information, we define a lexicographic progress measure which
ensures termination of this search. The main idea is as follows: the first progress
measure is to check if there a time-elapse t transition possible between (s, ν) and
(s
, ν
) and if so, we print this out. If not, ν
= ν + t, and some set of clocks
have been reset in the transition(s) from (s, ν) to (s
, ν
). The second progress
measure looks at the sequence of transitions from (s, ν) to (s
, ν
), consisting of
reset transitions (at most the number of clocks) that result in ν
from ν. If neither
the first nor the second progress measure apply, then ν = ν
, and we are left to
explore the last progress measure, by exploring at most |S| number of transitions
from (s, ν) to (s
, ν
). Using this progress measure, we can seamlessly extend the
witness generation to the timed setting. The challenges involved therein, can be
seen in the full version [4].