Skip to content Skip to navigation
University of Warwick
  • Study
  • |
  • Research
  • |
  • Business
  • |
  • Alumni
  • |
  • News
  • |
  • About

University of Warwick
Publications service & WRAP

Highlight your research

  • WRAP
    • Home
    • Search WRAP
    • Browse by Warwick Author
    • Browse WRAP by Year
    • Browse WRAP by Subject
    • Browse WRAP by Department
    • Browse WRAP by Funder
    • Browse Theses by Department
  • Publications Service
    • Home
    • Search Publications Service
    • Browse by Warwick Author
    • Browse Publications service by Year
    • Browse Publications service by Subject
    • Browse Publications service by Department
    • Browse Publications service by Funder
  • Help & Advice
University of Warwick

The Library

  • Login
  • Admin

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.

[img]
Preview
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

Request Changes to record.

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:
DateEvent
22 March 2016Available
8 January 2016Accepted
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:
  • Other Repository
  • Organisation
  • Publisher

Request changes or add full text files to a record

Repository staff actions (login required)

View Item View Item

Downloads

Downloads per month over past year

View more statistics

twitter

Email us: wrap@warwick.ac.uk
Contact Details
About Us