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.