Deciding structural liveness of Petri nets
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F61989100%3A27240%2F17%3A10238579" target="_blank" >RIV/61989100:27240/17:10238579 - isvavai.cz</a>
Result on the web
<a href="https://link.springer.com/chapter/10.1007%2F978-3-319-51963-0_8" target="_blank" >https://link.springer.com/chapter/10.1007%2F978-3-319-51963-0_8</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-51963-0_8" target="_blank" >10.1007/978-3-319-51963-0_8</a>
Alternative languages
Result language
angličtina
Original language name
Deciding structural liveness of Petri nets
Original language description
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 the verification of safety and liveness properties in this model; despite the extensive research effort, some basic problems remain open, which is exemplified by the open complexity status of the reachability problem. The liveness problems are known to be closely related to the reachability problem, and many structural properties of nets that are related to liveness have been studied. Somewhat surprisingly, the decidability status of the problem if a net is structurally live, i.e. if there is an initial marking for which it is live, has remained open, as also a recent paper (Best and Esparza, 2016) emphasizes. Here we show that the structural liveness problem for Petri nets is decidable. A crucial ingredient of the proof is the result by Leroux (LiCS 2013) showing that we can compute a finite (Presburger) description of the reachability set for a marked Petri net if this set is semilinear.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GA15-13784S" target="_blank" >GA15-13784S: Computational complexity of selected verification problems</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2017
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Volume 10139
ISBN
978-3-319-51962-3
ISSN
0302-9743
e-ISSN
neuvedeno
Number of pages
12
Pages from-to
"91-"--102
Publisher name
Springer
Place of publication
Berlin
Event location
Limerik
Event date
Jan 16, 2017
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000418793100008