Robustness of Time Petri Nets under Guard Enlargement

Sundararaman Akshay 1 Loïc Hélouët 2 Claude Jard 3 Pierre-Alain Reynier 4
1 Department of Computer Science and Engineering [Bombay]
2 SUMO - SUpervision of large MOdular and distributed systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
3 AELOS
LINA - Laboratoire d'Informatique de Nantes Atlantique
4 MOVE - Modélisation et Vérification
LIF - Laboratoire d'informatique Fondamentale de Marseille
Abstract : Robustness of timed systems aims at studying whether infinitesimal perturbations in clock values can result in new discrete behaviors. A model is robust if the set of discrete behav- iors is preserved under arbitrarily small (but positive) perturbations. We tackle this problem for time Petri nets (TPNs, for short) by considering the model of parametric guard enlargement which allows time-intervals constraining the firing of transitions in TPNs to be enlarged by a (positive) parameter. We show that TPNs are not robust in general and checking if they are robust with respect to standard properties (such as boundedness, safety) is undecidable. We then extend the marking class timed automaton construction for TPNs to a parametric setting, and prove that it is compatible with guard enlargements. We apply this result to the (undecidable) class of TPNs which are robustly bounded (i.e., whose finite set of reachable markings remains finite under infinitesimal perturbations): we provide two decidable robustly bounded subclasses, and show that one can effectively build a timed automaton which is timed bisimilar even in presence of perturbations. This allows us to apply existing results for timed automata to these TPNs and show further robustness properties.
Keywords : timed automata Robustness Petri nets
Type de document :
Article dans une revue
Fundamenta Informaticae, Polskie Towarzystwo Matematyczne, 2016, 143 (3-4), pp.207-234. 〈10.3233/FI-2016-1312〉
Liste complète des métadonnées
https://hal.inria.fr/hal-01379431
Contributeur : Loic Helouet <>
Soumis le : mardi 11 octobre 2016 - 15:01:43
Dernière modification le : samedi 21 juillet 2018 - 14:12:01

Lien texte intégral

openaccess

Identifiants

Collections

LINA | EC-MARSEILLE | UNIV-NANTES | INRIA | IRISA | UNIV-AMU | UR1-UFR-ISTIC | CENTRALESUPELEC | LINA-AELOS | LIF | LIS-LAB | MOVE | UNIV-RENNES

Citation

Sundararaman Akshay, Loïc Hélouët, Claude Jard, Pierre-Alain Reynier. Robustness of Time Petri Nets under Guard Enlargement . Fundamenta Informaticae, Polskie Towarzystwo Matematyczne, 2016, 143 (3-4), pp.207-234. 〈10.3233/FI-2016-1312〉. 〈hal-01379431〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

1252

Contact


archive-ouverte@inria.fr