*For the most recent entries see the
Petri Nets Newsletter.*

## Decidability of Zenoness, Syntactic Boundedness and Token-Liveness for Dense-Timed Petri Nets.

Abdulla, Parosh;
Mahata, Pritha;
Mayr, Richard
In:
Kamal Lodaya, Meena Mahajan (Eds.): *Lecture Notes in Computer Science, Vol. 3328: FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science: 24th International Conference, Chennai, India, December 16-18, 2004*, pages 58-70.
Springer-Verlag,
2004.

Abstract:
We consider Timed Petri Nets (TPNs) : extensions of Petri nets in which
each token is equipped with a real-valued clock. We consider the following
three verification problems for TPNs. (i) Zenoness: whether there is an
infinite computation from a given marking which takes only a finite amount
of time. We show decidability of zenoness for TPNs, thus solving an open
problem from [dFERA00]. (ii) Token Liveness: whether a token is alive in a
marking, i.e., whether there is a computation from the marking which
eventually consumes the token.We show decidability of the problem by
reducing it to the coverability problem,which is decidable for TPNs.
(iii)Boundedness: whether the size of the reachable markings is bounded.
We consider two versions of the problem; namely semantic boundednesswhere
only live tokens are taken into consideration in the markings,and
syntactic boundedness where also dead tokens are considered. We show
undecidability of semantic boundedness, while we prove that syntactic
boundedness is decidable through an extension of the Karp-Miller algorithm.

*Do you need a refined search? Try our search engine
which allows complex field-based queries.*
*Back to the Petri Nets Bibliography*