08/07/2020

Efficient Analysis of VASS Termination Complexity

Antonín Kučera, Jérôme Leroux and Dominik Velan

Keywords: Vector Addition Systems, Termination

Abstract: The termination complexity of a given VASS is a function L assigning to every n the length of the longest non-terminating 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 ϵ Gk, where Gk is the k-th level in the Grzegorczyk hierarchy, is decidable in polynomial time. Furthermore, we show that if L ϵ G, then L grows at least as fast as the generator Fk+1 of Gk+1. Hence, for every terminating VASS, the growth of L can be reasonably characterized by the least k such that L ϵ Gk. 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 ϵ Gk for a given VASS game is NP-complete. Furthermore, if L ϵ Gk, then L grows at least as fast as Fk+1.

 0
 0
 0
 0
This is an embedded video. Talk and the respective paper are published at ICALP 2020 virtual conference. If you are one of the authors of the paper and want to manage your upload, see the question "My papertalk has been externally embedded..." in the FAQ section.

Comments

Post Comment
no comments yet
code of conduct: tbd

Similar Papers