Combining Free Choice and Time in Petri Nets - IMT - Institut Mines-Télécom Accéder directement au contenu
Communication Dans Un Congrès Année : 2016

Combining Free Choice and Time in Petri Nets

Résumé

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.
Fichier principal
Vignette du fichier
FCTPN(Time2016).pdf (346.71 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01379440 , version 1 (11-10-2016)

Identifiants

  • HAL Id : hal-01379440 , version 1

Citer

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⟩
230 Consultations
130 Téléchargements

Partager

Gmail Facebook X LinkedIn More