Skip to Main content Skip to Navigation
Conference papers

Combining Free Choice and Time in Petri Nets

Abstract : Time Petri nets (TPNs) (Merlin 1974) 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 enabling 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 under a multi-server semantics. In particular, we show that the questions of fireability (whether a chosen transition can fire), and termination (whether the net has a non-terminating run) are decidable for this class. We then consider the problem of robustness under guard enlargement (Puri et al. 2000), i.e., whether a given property is preserved even if the system is implemented on an architecture with imprecise time measurement. This question was studied for TPNs in (Akshay et al. 2016), and decidability of several problems was obtained for bounded classes of nets. We show that robustness of fireability is decidable for unbounded free choice TPNs with a multi-server semantics.
Document type :
Conference papers
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/hal-01379440
Contributor : Loic Helouet <>
Submitted on : Tuesday, October 11, 2016 - 3:08:26 PM
Last modification on : Thursday, January 7, 2021 - 4:11:52 PM
Long-term archiving on: : Saturday, February 4, 2017 - 7:04:59 PM

File

FCTPN(Time2016).pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01379440, version 1

Citation

Sundararaman Akshay, Loïc Hélouët, Ramchandra Phawade. Combining Free Choice and Time in Petri Nets. 23rd International Symposium on Temporal Representation and Reasoning, Technical University of Denmark, Oct 2016, Lyngby, Denmark. pp.120-129. ⟨hal-01379440⟩

Share

Metrics

Record views

446

Files downloads

191