Combining Free choice and Time in Petri Nets - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2017

Combining Free choice and Time in Petri Nets

Résumé

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

Dates et versions

hal-01650751 , version 1 (28-11-2017)

Identifiants

  • HAL Id : hal-01650751 , version 1

Citer

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⟩
605 Consultations
131 Téléchargements

Partager

Gmail Facebook X LinkedIn More