Skip to Main content Skip to Navigation
Conference papers

Combining Free choice and Time in Petri Nets

Abstract : Time Petri nets (TPNs) are a classical extension of Petri nets with timing constraints attached to transitions, for which most verification problems are un- decidable. We consider TPNs under an urgent semantics with multiple enablings of transitions (frequently called ”multi-server semantics”). 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 multi-server semantics. Indeed, for this class of TPNs, several decision problems can be brought back to an untimed setting. 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. 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. There are several ways to model such imprecision. The first one is to consider the original model in which all guards are enlarged, to model possible clocks drifts. It is also frequent in the literature to model imprecision with guards shrinking, to encompass delays or advance in guards triggering. For unbounded free-choice TPNs with a multi-server semantics, we show de- cidability of robustness of firability and of termination under both guard enlarge- ment and shrinking. Up to our knowledge, this is the first decidability result for robustness in unbounded nets. Closely-related problems such as decidability of coverability and boundedness in free-choice TPNS and the associated robustness questions are still open issues.
Document type :
Conference papers
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Loic Helouet <>
Submitted on : Tuesday, November 28, 2017 - 2:37:42 PM
Last modification on : Thursday, January 7, 2021 - 4:34:54 PM


Files produced by the author(s)


  • HAL Id : hal-01650751, version 1


S Akshay, Loïc Hélouët, R Phawade. Combining Free choice and Time in Petri Nets . 6th IFIP Working group on trends in Concurrency, Sep 2017, Berlin, Germany. ⟨hal-01650751⟩



Record views


Files downloads