Dense-Timed Petri Nets: Checking Zenoness, Token liveness and Boundedness

We consider Dense-Timed Petri Nets (TPN), an extension of Petri nets in which each token is equipped with a real-valued clock and where the semantics is lazy (i.e., enabled transitions need not fire; time can pass and disable transitions). We consider the following verification problems for TPNs. (i...

Full description

Bibliographic Details
Main Authors: Parosh Abdulla, Pritha Mahata, Richard Mayr
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2007-02-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/2223/pdf