Coverability Trees for Petri Nets with Unordered Data

Abstract : We study an extension of classical Petri nets where tokens carry values from a countable data domain, that can be tested for equality upon firing transitions. These Unordered Data Petri Nets (UDPN) are well-structured and therefore allow generic decision procedures for several verification problems including coverability and boundedness. We show how to construct a finite representation of the coverability set in terms of its ideal decomposition. This not only provides an alternative method to decide coverability and boundedness, but is also an important step towards deciding the reachability problem. This also allows to answer more precise questions about the reachability set, for instance whether there is a bound on the number of tokens on a given place (place boundedness), or if such a bound exists for the number of different data values carried by tokens (place width boundedness). We provide matching Hyper-Ackermann bounds on the size of cover-ability trees and on the running time of the induced decision procedures.
Type de document :
Communication dans un congrès
FoSSaCS, 2016, Eindhoven, Netherlands. Springer, 9634, pp.445--461, Lecture Notes in Computer Science. <10.1007/978-3-662-49630-5_26>
Liste complète des métadonnées


https://hal.inria.fr/hal-01252674
Contributeur : Sylvain Schmitz <>
Soumis le : jeudi 7 janvier 2016 - 23:56:51
Dernière modification le : samedi 18 février 2017 - 01:14:43
Document(s) archivé(s) le : vendredi 8 avril 2016 - 13:37:12

Fichier

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

Identifiants

Citation

Piotr Hofman, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, Sylvain Schmitz, et al.. Coverability Trees for Petri Nets with Unordered Data. FoSSaCS, 2016, Eindhoven, Netherlands. Springer, 9634, pp.445--461, Lecture Notes in Computer Science. <10.1007/978-3-662-49630-5_26>. <hal-01252674>

Partager

Métriques

Consultations de
la notice

604

Téléchargements du document

156