Coverability Trees for Petri Nets with Unordered Data

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

doi:10.1007/978-3-662-49630-5_26

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 proceeding › Conference contribution

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.

Original language	English
Title of host publication	Foundations of Software Science and Computation Structures
Subtitle of host publication	19th 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 Publication	Eindhoven, Netherlands
Publisher	Springer Berlin Heidelberg
Number of pages	17
ISBN (Electronic)	978-3-662-49630-5
ISBN (Print)	978-3-662-49629-9
DOIs	https://doi.org/10.1007/978-3-662-49630-5_26
Publication status	Published - Mar 2016
Event	19th International Conference of Foundations of Software Science and Computation Structures - Eindhoven, Netherlands Duration: 2 Apr 2016 → 8 Apr 2016 https://www.etaps.org/index.php/2016

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg
Volume	9634
ISSN (Print)	0302-9743

Conference

Conference	19th International Conference of Foundations of Software Science and Computation Structures
Abbreviated title	FOSSACS 2016
Country/Territory	Netherlands
City	Eindhoven
Period	2/04/16 → 8/04/16
Internet address	https://www.etaps.org/index.php/2016

Access to Document

10.1007/978-3-662-49630-5_26

HLLLST2016Accepted author manuscript, 389 KB

Cite this

Hofman, P., Lasota, S., Lazi, R., Leroux, J., Schmitz, S., & Totzke, P. (2016). Coverability Trees for Petri Nets with Unordered Data. In Foundations of Software Science and Computation Structures: 19th 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 (Lecture Notes in Computer Science; Vol. 9634). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-662-49630-5_26

Hofman, Piotr ; Lasota, Slawomir ; Lazi, Ranko et al. / Coverability Trees for Petri Nets with Unordered Data. Foundations of Software Science and Computation Structures: 19th 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. Eindhoven, Netherlands : Springer Berlin Heidelberg, 2016. (Lecture Notes in Computer Science).

@inproceedings{ebb70f4391424a8db5a6d93c4536f1a1,

title = "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.",

author = "Piotr Hofman and Slawomir Lasota and Ranko Lazi and J{\'e}r{\^o}me Leroux and Sylvain Schmitz and Patrick Totzke",

year = "2016",

month = mar,

doi = "10.1007/978-3-662-49630-5_26",

language = "English",

isbn = "978-3-662-49629-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin Heidelberg",

booktitle = "Foundations of Software Science and Computation Structures",

note = "19th International Conference of Foundations of Software Science and Computation Structures , FOSSACS 2016 ; Conference date: 02-04-2016 Through 08-04-2016",

url = "https://www.etaps.org/index.php/2016",

}

Hofman, P, Lasota, S, Lazi, R, Leroux, J, Schmitz, S & Totzke, P 2016, Coverability Trees for Petri Nets with Unordered Data. in Foundations of Software Science and Computation Structures: 19th 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. Lecture Notes in Computer Science, vol. 9634, Springer Berlin Heidelberg, Eindhoven, Netherlands, 19th International Conference of Foundations of Software Science and Computation Structures , Eindhoven, Netherlands, 2/04/16. https://doi.org/10.1007/978-3-662-49630-5_26

Coverability Trees for Petri Nets with Unordered Data. / Hofman, Piotr; Lasota, Slawomir; Lazi, Ranko et al.

Foundations of Software Science and Computation Structures: 19th 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. Eindhoven, Netherlands : Springer Berlin Heidelberg, 2016. (Lecture Notes in Computer Science; Vol. 9634).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Coverability Trees for Petri Nets with Unordered Data

AU - Hofman, Piotr

AU - Lasota, Slawomir

AU - Lazi, Ranko

AU - Leroux, Jérôme

AU - Schmitz, Sylvain

AU - Totzke, Patrick

PY - 2016/3

Y1 - 2016/3

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-662-49630-5_26

DO - 10.1007/978-3-662-49630-5_26

M3 - Conference contribution

SN - 978-3-662-49629-9

T3 - Lecture Notes in Computer Science

BT - Foundations of Software Science and Computation Structures

PB - Springer Berlin Heidelberg

CY - Eindhoven, Netherlands

T2 - 19th International Conference of Foundations of Software Science and Computation Structures

Y2 - 2 April 2016 through 8 April 2016

ER -

Hofman P, Lasota S, Lazi R, Leroux J, Schmitz S, Totzke P. Coverability Trees for Petri Nets with Unordered Data. In Foundations of Software Science and Computation Structures: 19th 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. Eindhoven, Netherlands: Springer Berlin Heidelberg. 2016. (Lecture Notes in Computer Science). doi: 10.1007/978-3-662-49630-5_26

Coverability Trees for Petri Nets with Unordered Data

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this