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

Structural liveness of petri nets is ExpSpace-hard and decidable

Tools
- Tools
+ Tools

Jančar, Petr and Purser, David (2019) Structural liveness of petri nets is ExpSpace-hard and decidable. ACTA Informatica, 56 . pp. 537-552. doi:10.1007/s00236-019-00338-6 ISSN 0001-5903.

[img]
Preview
PDF
WRAP-structural-liveness-Petri-nets-Purser-2019.pdf - Accepted Version - Requires a PDF viewer.

Download (869Kb) | Preview
Official URL: https://doi.org/10.1007/s00236-019-00338-6

Request Changes to record.

Abstract

Place/transition Petri nets are a standard model for a class of distributed systems whose reachability spaces might be infinite. One of well-studied topics is verification of safety and liveness properties in this model; despite an extensive research effort, some basic problems remain open, which is exemplified by the complexity status of the reachability problem that is still not fully clarified. The liveness problems are known to be closely related to the reachability problem, and various structural properties of nets that are related to liveness have been studied. Somewhat surprisingly, the decidability status of the problem of determining whether a net is structurally live, i.e. whether there is an initial marking for which it is live, remained open for some time; e.g. Best and Esparza (Inf Process Lett 116(6):423–427, 2016. https://doi.org/10.1016/j.ipl.2016.01.011) emphasize this open question. Here we show that the structural liveness problem for Petri nets is ExpSpace-hard and decidable. In particular, given a net N and a semilinear set S, it is decidable whether there is an initial marking of N for which the reachability set is included in S; this is based on results by Leroux (28th annual ACM/IEEE symposium on logic in computer science, LICS 2013, New Orleans, LA, USA, June 25–28, 2013, IEEE Computer Society, pp 23–32, 2013. https://doi.org/10.1109/LICS.2013.7).

Item Type: Journal Article
Subjects: Q Science > QA Mathematics
T Technology > TA Engineering (General). Civil engineering (General)
Divisions: Faculty of Science, Engineering and Medicine > Science > Computer Science
Faculty of Science, Engineering and Medicine > Science > Mathematics
Library of Congress Subject Headings (LCSH): Petri nets , Computer algorithms
Journal or Publication Title: ACTA Informatica
Publisher: Springer
ISSN: 0001-5903
Official Date: 1 September 2019
Dates:
DateEvent
1 September 2019Published
8 July 2019Available
2 July 2019Accepted
Volume: 56
Page Range: pp. 537-552
DOI: 10.1007/s00236-019-00338-6
Status: Peer Reviewed
Publication Status: Published
Reuse Statement (publisher, data, author rights): This is a post-peer-review, pre-copyedit version of an article published in ACTA Informatica. The final authenticated version is available online at: https://doi.org/10.1007/s00236-019-00338-6
Access rights to Published version: Restricted or Subscription Access
Date of first compliant deposit: 5 July 2019
Date of first compliant Open Access: 8 July 2020
RIOXX Funder/Project Grant:
Project/Grant IDRIOXX Funder NameFunder ID
18-11193STechnology Agency of the Czech Republichttp://dx.doi.org/10.13039/100014809
EP/L016400/1[EPSRC] Engineering and Physical Sciences Research Councilhttp://dx.doi.org/10.13039/501100000266
Related URLs:
  • 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