Efficient Analysis of VASS Termination Complexity

D 2020

Efficient Analysis of VASS Termination Complexity

KUČERA, Antonín, Jérôme LEROUX a Dominik VELAN

Základní údaje

Originální název

Efficient Analysis of VASS Termination Complexity

Autoři

KUČERA, Antonín (203 Česká republika, garant, domácí), Jérôme LEROUX (250 Francie) a Dominik VELAN (203 Česká republika, domácí)

Vydání

New York, USA, LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, od s. 676-688, 13 s. 2020

Nakladatel

ACM

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10200 1.2 Computer and information sciences

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Kód RIV

RIV/00216224:14330/20:00114250

Organizační jednotka

Fakulta informatiky

ISBN

978-1-4503-7104-9

DOI

http://dx.doi.org/10.1145/3373718.3394751

UT WoS

000665014900052

Klíčová slova anglicky

Vector addition systems; Termination

Štítky

core_A, firank_1

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 29. 4. 2021 07:59, RNDr. Pavel Šmerk, Ph.D.

Anotace

ORIG CZ

V originále

The termination complexity of a given VASS is a function $L$ assigning to every $n$ the length of the longest nonterminating computation initiated in a configuration with all counters bounded by $n$. We show that for every VASS with demonic nondeterminism and every fixed $k$, the problem whether $L \in G_k$, where $G_k$ is the $k$-th level in the Grzegorczyk hierarchy, is decidable in polynomial time. Furthermore, we show that if $L \notin G_k$, then L grows at least as fast as the generator $F_k+1$ of $G_k+1$. Hence, for every terminating VASS, the growth of $L$ can be reasonably characterized by the least $k$ such that $L \in G_k$. Furthermore, we consider VASS with both angelic and demonic nondeterminism, i.e., VASS games where the players aim at lowering/raising the termination time. We prove that for every fixed $k$, the problem whether $L \in G_k$ for a given VASS game is NP-complete. Furthermore, if $L \notin G_k$, then $L$ grows at least as fast as $F_k+1$.

Česky

Článek se zabývá odhadem maximální doby běhu VASS systémů.

Návaznosti

GA18-11193S, projekt VaV

Název: Algoritmy pro diskrétní systémy a hry s nekonečně mnoha stavy

Investor: Grantová agentura ČR, Algoritmy pro diskrétní systémy a hry s nekonečně mnoha stavy

MUNI/A/1050/2019, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX (Akronym: SV-FI MAV IX)

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

MUNI/A/1076/2019, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 20 (Akronym: SKOMU)

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 20, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

KUČERA, Antonín, Jérôme LEROUX a Dominik VELAN. Efficient Analysis of VASS Termination Complexity. Online. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, Dale Miller. LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. New York, USA: ACM, 2020, s. 676-688. ISBN 978-1-4503-7104-9. Dostupné z: https://dx.doi.org/10.1145/3373718.3394751.

@inproceedings{1672264,
   author = {Kučera, Antonín and Leroux, Jérôme and Velan, Dominik},
   address = {New York, USA},
   booktitle = {LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science},
   doi = {http://dx.doi.org/10.1145/3373718.3394751},
   editor = {Holger Hermanns, Lijun Zhang, Naoki Kobayashi, Dale Miller},
   keywords = {Vector addition systems; Termination},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {New York, USA},
   isbn = {978-1-4503-7104-9},
   pages = {676-688},
   publisher = {ACM},
   title = {Efficient Analysis of VASS Termination Complexity},
   year = {2020}
}

TY  - JOUR
ID  - 1672264
AU  - Kučera, Antonín - Leroux, Jérôme - Velan, Dominik
PY  - 2020
TI  - Efficient Analysis of VASS Termination Complexity
PB  - ACM
CY  - New York, USA
SN  - 9781450371049
KW  - Vector addition systems
KW  - Termination
N2  - The termination complexity of a given VASS is a function $L$ assigning to every $n$ the length of the longest nonterminating computation initiated in a configuration with all counters bounded by $n$. We show that for every VASS with demonic nondeterminism and every fixed $k$, the problem whether $L \in G_k$, where $G_k$ is the $k$-th level in the Grzegorczyk hierarchy, is decidable in polynomial time. Furthermore, we show that if $L \notin G_k$, then L grows at least as fast as the generator $F_k+1$ of $G_k+1$. Hence, for every terminating VASS, the growth of $L$ can be reasonably characterized by the least $k$ such that $L \in G_k$. Furthermore, we consider VASS with both angelic and demonic nondeterminism, i.e., VASS games where the players aim at lowering/raising the termination time. We prove that for every fixed $k$, the problem whether $L \in G_k$ for a given VASS game is NP-complete. Furthermore, if $L \notin G_k$, then $L$ grows at least as fast as $F_k+1$.
ER  -

KUČERA, Antonín, Jérôme LEROUX a Dominik VELAN. Efficient Analysis of VASS Termination Complexity. Online. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, Dale Miller. \textit{LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science}. New York, USA: ACM, 2020, s.~676-688. ISBN~978-1-4503-7104-9. Dostupné z: https://dx.doi.org/10.1145/3373718.3394751.

Podrobný výpis o publikaci