The Library
Coverability trees for petri nets with unordered data
Tools
Tools
Tools
Hofman, Piotr , Lasota, Slawomir , Lazic, Ranko, Leroux, Jerome , Schmitz, Sylvain and Totzke, Patrick (2016) Coverability trees for petri nets with unordered data. In: 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Eindhoven, The Netherlands, 2-8 Apr 2016. Published in: Lecture Notes in Computer Science, 9634 pp. 445-461. ISBN 9783662496299. doi:10.1007/978-3-662-49630-5_26 ISSN 0302-9743.
|
PDF
WRAP_main.pdf - Accepted Version - Requires a PDF viewer. Download (723Kb) | Preview |
Official URL: http://dx.doi.org/10.1007/978-3-662-49630-5_26
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.
| Item Type: | Conference Item (Paper) | ||||||
|---|---|---|---|---|---|---|---|
| Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||||
| Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||||
| Library of Congress Subject Headings (LCSH): | Petri nets -- Research | ||||||
| Journal or Publication Title: | Lecture Notes in Computer Science | ||||||
| Publisher: | Springer | ||||||
| ISBN: | 9783662496299 | ||||||
| ISSN: | 0302-9743 | ||||||
| Official Date: | 22 March 2016 | ||||||
| Dates: |
|
||||||
| Volume: | 9634 | ||||||
| Page Range: | pp. 445-461 | ||||||
| DOI: | 10.1007/978-3-662-49630-5_26 | ||||||
| Status: | Peer Reviewed | ||||||
| Publication Status: | Published | ||||||
| Access rights to Published version: | Restricted or Subscription Access | ||||||
| Date of first compliant deposit: | 3 March 2016 | ||||||
| Date of first compliant Open Access: | 18 May 2016 | ||||||
| Funder: | Narodowe Centrum Nauki (NCN), Labex Digicosme, Université Paris-Saclay (UPS), Engineering and Physical Sciences Research Council (EPSRC), France. Agence nationale de la recherche (ANR), Leverhulme Trust (LT) | ||||||
| Grant number: | 2012/07/B/ST6/01497 2013/09/B/ST6/01575 (NCN), VERICONISS (UPS), EP/M011801/1 (EPSRC), NR-14-CE28-0005 (ANR), VP1-2014-041 (LT)) | ||||||
| Conference Paper Type: | Paper | ||||||
| Title of Event: | 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS) | ||||||
| Type of Event: | Conference | ||||||
| Location of Event: | Eindhoven, The Netherlands | ||||||
| Date(s) of Event: | 2-8 Apr 2016 | ||||||
| Related URLs: |
Request changes or add full text files to a record
Repository staff actions (login required)
 |
View Item |
Downloads
Downloads per month over past year
