Deciding structural liveness of Petri nets

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Deciding structural liveness of Petri nets

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Deciding structural liveness of Petri nets

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA15-13784S" target="_blank" >GA15-13784S: Výpočetní složitost vybraných verifikačních problémů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2017

Kód důvěrnosti údajů

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

Název statě ve sborníku

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

Počet stran výsledku

12

Strana od-do

"91-"--102

Název nakladatele

Springer

Místo vydání

Berlin

Místo konání akce

Limerik

Datum konání akce

16. 1. 2017

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000418793100008