Deciding Polynomial Termination Complexity for VASS Programs

TL;DR

This paper classifies the computational complexity of determining polynomial termination and complexity bounds for VASS programs, revealing inherent difficulty and identifying tractable subclasses based on structural parameters.

Contribution

It provides a detailed complexity classification for polynomial termination problems in VASS and VASS games, extending previous results and identifying conditions for tractability.

Findings

Complexity classifications for fixed k in VASS termination problems.

NP-completeness, coNP-completeness, and DP-completeness results.

PSPACE-completeness for VASS games and identification of tractable subclasses.

Abstract

We show that for every fixed $k\geq 3$, the problem whether the termination/counter complexity of a given demonic VASS is $\mathcal{O}(n^k)$, $\Omega(n^{k})$, and $\Theta(n^{k})$ is coNP-complete, NP-complete, and DP-complete, respectively. We also classify the complexity of these problems for $k\leq 2$. This shows that the polynomial-time algorithm designed for strongly connected demonic VASS in previous works cannot be extended to the general case. Then, we prove that the same problems for VASS games are PSPACE-complete. Again, we classify the complexity also for $k\leq 2$. Interestingly, tractable subclasses of demonic VASS and VASS games are obtained by bounding certain structural parameters, which opens the way to applications in program analysis despite the presented lower complexity bounds.