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 undecidable. We consider TPNs under a strong semantics with multiple enablings 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 in the timed setting under a multi-server semantics. 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 for this class. 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. For unbounded free choice TPNs with a multi-server semantics, we show decidability of robustness of firability and of termination under both guard enlargement and shrinking.
Type de document :
Rapport
[Research Report] INRIA Rennes - Bretagne Atlantique. 2017
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01646913
Contributeur : Loic Helouet <>
Soumis le : jeudi 23 novembre 2017 - 21:53:11
Dernière modification le : jeudi 12 avril 2018 - 01:54:57

Fichier

Lamp.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01646913, version 1

Citation

S Akshay, Loïc Hélouët, Ramchandra Phawade. Combining Free choice and Time in Petri Nets. [Research Report] INRIA Rennes - Bretagne Atlantique. 2017. 〈hal-01646913〉

Partager

Métriques

Consultations de la notice

108

Téléchargements de fichiers

16