Abstract

Dense-Timed Petri Nets are an extension of Petri nets in which each
token is equipped with a real-valued clock.
The Zeno problem is the question whether there exists a
Zeno-computation from a given marking, i.e., an infinite computation
which takes only a finite amount of time.
This question is hard for dense time, because (unlike for discrete time)
an infinite Zeno-computation can have infinitely many time-passing phases
of decreasing length (e.g., 2^{-n}, for n=1,2,...).
We show the decidability of the Zeno problem by a (partial) encoding
of timed Petri nets into a subclass of untimed transfer nets.
Furthermore, the related question if there exist arbitrarily fast
computations from a given marking in a timed Petri net
is also decidable.
On the other hand, the existence of an infinite non-Zeno computation
(i.e., an infinite computation taking infinite time) is undecidable.