Efficient Analysis of VASS Termination Complexity

D 2020

Efficient Analysis of VASS Termination Complexity

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

Basic information

Original name

Efficient Analysis of VASS Termination Complexity

Authors

KUČERA, Antonín (203 Czech Republic, guarantor, belonging to the institution), Jérôme LEROUX (250 France) and Dominik VELAN (203 Czech Republic, belonging to the institution)

Edition

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

Publisher

ACM

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10200 1.2 Computer and information sciences

Confidentiality degree

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

Publication form

electronic version available online

RIV identification code

RIV/00216224:14330/20:00114250

Organization unit

Faculty of Informatics

ISBN

978-1-4503-7104-9

DOI

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

UT WoS

000665014900052

Keywords in English

Vector addition systems; Termination

Abstract

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

In Czech

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

Links

GA18-11193S, research and development project

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

Investor: Czech Science Foundation

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

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

Investor: Masaryk University, Category A

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

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

Investor: Masaryk University, Category A

Citovat

KUČERA, Antonín, Jérôme LEROUX and 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, p. 676-688. ISBN 978-1-4503-7104-9. Available from: 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 and 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, p.~676-688. ISBN~978-1-4503-7104-9. Available from: https://dx.doi.org/10.1145/3373718.3394751.

Detailed Information on Publication Record