The Library
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
|
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
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 > Computer Science Faculty of 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: |
|
|||||||||
| Volume: | 56 | |||||||||
| Page Range: | pp. 537-552 | |||||||||
| DOI: | 10.1007/s00236-019-00338-6 | |||||||||
| Status: | Peer Reviewed | |||||||||
| Publication Status: | Published | |||||||||
| Publisher Statement: | 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 | |||||||||
| RIOXX Funder/Project Grant: |
|
|||||||||
| 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
