Efficient Analysis of VASS Termination Complexity

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F20%3A00114250" target="_blank" >RIV/00216224:14330/20:00114250 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1145/3373718.3394751" target="_blank" >http://dx.doi.org/10.1145/3373718.3394751</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1145/3373718.3394751" target="_blank" >10.1145/3373718.3394751</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Efficient Analysis of VASS Termination Complexity

Popis výsledku v původním jazyce

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

Název v anglickém jazyce

Efficient Analysis of VASS Termination Complexity

Popis výsledku anglicky

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

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10200 - Computer and information sciences

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í

2020

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

LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science

ISBN

9781450371049

ISSN

—

e-ISSN

—

Počet stran výsledku

13

Strana od-do

676-688

Název nakladatele

ACM

Místo vydání

New York, USA

Místo konání akce

Saarbrucken, Germany

Datum konání akce

1. 1. 2020

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

WRD - Celosvětová akce

Kód UT WoS článku

000665014900052