Skip to Main content Skip to Navigation
Journal articles

Combining Free choice and Time in Petri Nets

Sundararaman Akshay 1 Loïc Hélouët 2, * Ramchandra Phawade 3
* Corresponding author
2 SUMO - SUpervision of large MOdular and distributed systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Time Petri nets (TPNs) are a classical extension of Petri nets with timing constraints attached to transitions , for which most verification problems are undecidable. We consider TPNs under a strong semantics with multiple enablings of transitions. We focus on a structural subclass of unbounded TPNs, where the underlying untimed net is free choice, and show that it enjoys nice properties in the timed setting under a multi-enabling semantics. In particular, we show that the questions of firability (whether a chosen transition can fire), and termination (whether the net has a non-terminating run) are decidable for this class. Next, we consider the problem of robustness under guard enlargement and guard shrinking, i.e., whether a given property is preserved even if the system is implemented on an architecture with imprecise time measurement. For unbounded free choice TPNs with a multi-enabling semantics, we show decidability of robustness of firability and of termination under both guard enlargement and shrinking.
Document type :
Journal articles
Complete list of metadata

Cited literature [35 references]  Display  Hide  Download
Contributor : Loic Helouet <>
Submitted on : Thursday, November 22, 2018 - 9:25:23 PM
Last modification on : Wednesday, February 17, 2021 - 2:49:43 PM
Long-term archiving on: : Saturday, February 23, 2019 - 4:19:50 PM


Files produced by the author(s)



Sundararaman Akshay, Loïc Hélouët, Ramchandra Phawade. Combining Free choice and Time in Petri Nets. Journal of Logical and Algebraic Methods in Programming, Elsevier, 2020, pp.1-36. ⟨10.1016/j.jlamp.2018.11.006⟩. ⟨hal-01931728⟩



Record views


Files downloads