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.
Type de document :
Communication dans un congrès
6th IFIP Working group on trends in Concurrency, Sep 2017, Berlin, Germany. 2017
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger
Contributeur : Loic Helouet <>
Soumis le : mardi 28 novembre 2017 - 14:37:42
Dernière modification le : mercredi 21 février 2018 - 01:26:55


Fichiers produits par l'(les) auteur(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. 2017. 〈hal-01650751〉



Consultations de la notice


Téléchargements de fichiers