Co-finiteness and Co-emptiness of Reachability Sets in Vector Addition Systems with States

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F61989592%3A15310%2F18%3A73588846" target="_blank" >RIV/61989592:15310/18:73588846 - isvavai.cz</a>

Výsledek na webu

<a href="https://link.springer.com/chapter/10.1007%2F978-3-319-91268-4_10" target="_blank" >https://link.springer.com/chapter/10.1007%2F978-3-319-91268-4_10</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-91268-4_10" target="_blank" >10.1007/978-3-319-91268-4_10</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Co-finiteness and Co-emptiness of Reachability Sets in Vector Addition Systems with States

Popis výsledku v původním jazyce

The coverability and boundedness problems are well-known exponential-space complete problems for vector addition systems with states (or Petri nets). The boundedness problem asks if the reachability set (for a given initial configuration) is finite. Here we consider a dual problem, the co-finiteness problem that asks if the complement of the reachability set is finite; by restricting the question we get the co-emptiness (or universality) problem that asks if all configurations are reachable. We show that both the co-finiteness problem and the co-emptiness problem are complete for exponential space. While the lower bounds are obtained by a straightforward reduction from coverability, getting the upper bounds is more involved; in particular we use the bounds derived for reversible reachability by Leroux in 2013. The studied problems have been motivated by a recent result for structural liveness of Petri nets; this problem has been shown decidable by Jančar in 2017 but its complexity has not been clarified. The problem is tightly related to a generalization of the co-emptiness problem for non-singleton sets of initial markings, in particular for downward closed sets. We formulate the problems generally for semilinear sets of initial markings, and in this case we show that the co-emptiness problem is decidable (without giving an upper complexity bound) and we formulate a conjecture under which the co-finiteness problem is also decidable.

Název v anglickém jazyce

Co-finiteness and Co-emptiness of Reachability Sets in Vector Addition Systems with States

Popis výsledku anglicky

The coverability and boundedness problems are well-known exponential-space complete problems for vector addition systems with states (or Petri nets). The boundedness problem asks if the reachability set (for a given initial configuration) is finite. Here we consider a dual problem, the co-finiteness problem that asks if the complement of the reachability set is finite; by restricting the question we get the co-emptiness (or universality) problem that asks if all configurations are reachable. We show that both the co-finiteness problem and the co-emptiness problem are complete for exponential space. While the lower bounds are obtained by a straightforward reduction from coverability, getting the upper bounds is more involved; in particular we use the bounds derived for reversible reachability by Leroux in 2013. The studied problems have been motivated by a recent result for structural liveness of Petri nets; this problem has been shown decidable by Jančar in 2017 but its complexity has not been clarified. The problem is tightly related to a generalization of the co-emptiness problem for non-singleton sets of initial markings, in particular for downward closed sets. We formulate the problems generally for semilinear sets of initial markings, and in this case we show that the co-emptiness problem is decidable (without giving an upper complexity bound) and we formulate a conjecture under which the co-finiteness problem is also decidable.

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/GA18-11193S" target="_blank" >GA18-11193S: Algoritmy pro diskrétní systémy a hry s nekonečně mnoha stavy</a><br>

Návaznosti

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

Rok uplatnění

2018

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

39th International Conference on Application and Theory of Petri Nets and Concurrency

ISBN

978-3-319-91267-7

ISSN

0302-9743

e-ISSN

neuvedeno

Počet stran výsledku

20

Strana od-do

184-203

Název nakladatele

Springer-Verlag

Místo vydání

Dordrecht

Místo konání akce

Bratislava

Datum konání akce

24. 6. 2018

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

WRD - Celosvětová akce

Kód UT WoS článku

—