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%2F19%3A73597332" target="_blank" >RIV/61989592:15310/19:73597332 - isvavai.cz</a>

Výsledek na webu

<a href="https://content.iospress.com/articles/fundamenta-informaticae/fi1841" target="_blank" >https://content.iospress.com/articles/fundamenta-informaticae/fi1841</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.3233/FI-2019-1841" target="_blank" >10.3233/FI-2019-1841</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 boundedness problem is a well-known exponential-space complete problem for vector addition systems with states (or Petri nets); it 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 exponential-space complete. 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 (2013). The studied problems were motivated by a result for structural liveness of Petri nets; this problem was shown decidable by Jancar (2017), without clarifying its complexity. The structural liveness problem is tightly related to a generalization of the co-emptiness problem, where the sets of initial configurations are (possibly infinite) downward closed sets instead of just singletons. We formulate the problems even more generally, for semilinear sets of initial configurations; 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 boundedness problem is a well-known exponential-space complete problem for vector addition systems with states (or Petri nets); it 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 exponential-space complete. 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 (2013). The studied problems were motivated by a result for structural liveness of Petri nets; this problem was shown decidable by Jancar (2017), without clarifying its complexity. The structural liveness problem is tightly related to a generalization of the co-emptiness problem, where the sets of initial configurations are (possibly infinite) downward closed sets instead of just singletons. We formulate the problems even more generally, for semilinear sets of initial configurations; 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

J_imp - Článek v periodiku v databázi Web of Science

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í

2019

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 periodika

FUNDAMENTA INFORMATICAE

ISSN

0169-2968

e-ISSN

—

Svazek periodika

169

Číslo periodika v rámci svazku

1-2

Stát vydavatele periodika

PL - Polská republika

Počet stran výsledku

28

Strana od-do

123-150

Kód UT WoS článku

000489900300006

EID výsledku v databázi Scopus

2-s2.0-85073729714