Efficient Analysis of VASS Termination Complexity

Investor logo

Warning

This publication doesn't include Faculty of Sports Studies. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

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

Year of publication 2020
Type Article in Proceedings
Conference LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1145/3373718.3394751
Keywords Vector addition systems; Termination
Description 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$.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.

More info