Decidable Classes of Unbounded Petri Nets with Time and Urgency

Abstract : Adding real time information to Petri net models often leads to un-decidability of classical verification problems such as reachability and bounded-ness. For instance, models such as Timed-Transition Petri nets (TPNs) are intractable except in a bounded setting. On the other hand, the model of Timed-Arc Petri nets enjoys decidability results for boundedness and control-state reachability problems at the cost of disallowing urgency (the ability to enforce actions within a time delay). Our goal is to investigate decidable classes of Petri nets with time that capture some urgency and still allow unbounded behaviors, which go beyond finite state systems. We present, up to our knowledge, the first decidability results on reachability and boundedness for Petri net variants that combine unbounded places, time, and urgency. For this, we introduce the class of Timed-Arc Petri nets with restricted Urgency, where urgency can be used only on transitions consuming tokens from bounded places. We show that control-state reachability and boundedness are de-cidable for this new class, by extending results from Timed-Arc Petri nets (without urgency). Our main result concerns (marking) reachability, which is un-decidable for both TPNs (because of unrestricted urgency) [20] and Timed-Arc Petri Nets (because of infinite number of " clocks "). We obtain decidability of reachability for unbounded TPNs with restricted urgency under a new, yet natural , timed-arc semantics presenting them as Timed-Arc Petri Nets with restricted urgency. Decidability of reachability under the intermediate marking semantics is also obtained for a restricted subclass.
Type de document :
Communication dans un congrès
Fabrice Kordon and Daniel Moldt. Application and Theory of Petri Nets and Concurrency - 37th International Conference, PETRI NETS, 2016, Jun 2016, Torun, Poland. Springer, Lecture Notes in Computer Science, pp.301 - 322, 2016, Application and Theory of Petri Nets and Concurrency - 37th International Conference, PETRI NETS, 2016. 〈http://acsd2016.mat.umk.pl/〉. 〈10.1007/978-3-319-39086-4_18〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01379414
Contributeur : Loic Helouet <>
Soumis le : mardi 11 octobre 2016 - 14:49:28
Dernière modification le : samedi 21 juillet 2018 - 14:12:01
Document(s) archivé(s) le : samedi 4 février 2017 - 19:01:26

Fichier

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

Identifiants

Citation

Sundararaman Akshay, Blaise Genest, Loïc Hélouët. Decidable Classes of Unbounded Petri Nets with Time and Urgency. Fabrice Kordon and Daniel Moldt. Application and Theory of Petri Nets and Concurrency - 37th International Conference, PETRI NETS, 2016, Jun 2016, Torun, Poland. Springer, Lecture Notes in Computer Science, pp.301 - 322, 2016, Application and Theory of Petri Nets and Concurrency - 37th International Conference, PETRI NETS, 2016. 〈http://acsd2016.mat.umk.pl/〉. 〈10.1007/978-3-319-39086-4_18〉. 〈hal-01379414〉

Partager

Métriques

Consultations de la notice

322

Téléchargements de fichiers

78