Deciding structural liveness of Petri nets

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>

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

—

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)

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)

Publication year

2017

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

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