Coverability Trees for Petri Nets with Unordered Data

Piotr Hofman, Slawomir Lasota, Ranko Lazi, Jérôme Leroux, Sylvain Schmitz, Patrick Totzke

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures
Subtitle of host publication19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings
Place of PublicationEindhoven, Netherlands
PublisherSpringer Berlin Heidelberg
Number of pages17
ISBN (Electronic)978-3-662-49630-5
ISBN (Print)978-3-662-49629-9
DOIs
Publication statusPublished - Mar 2016
Event19th International Conference of Foundations of Software Science and Computation Structures - Eindhoven, Netherlands
Duration: 2 Apr 20168 Apr 2016
https://www.etaps.org/index.php/2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume9634
ISSN (Print)0302-9743

Conference

Conference19th International Conference of Foundations of Software Science and Computation Structures
Abbreviated titleFOSSACS 2016
Country/TerritoryNetherlands
CityEindhoven
Period2/04/168/04/16
Internet address

Fingerprint

Dive into the research topics of 'Coverability Trees for Petri Nets with Unordered Data'. Together they form a unique fingerprint.

Cite this