Deciding Polynomial Termination Complexity for VASS Programs

2021/02/13 by Ajdarów, Michal, Kučera, Antonín
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2102.06889

Abstract

We show that for every fixed k≥ 3, the problem whether the termination/counter complexity of a given demonic VASS is O(n^k), Ω(n^k), and Θ(n^k) is coNP-complete, NP-complete, and DP-complete, respectively. We also classify the complexity of these problems for k≤ 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≤ 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.

Related

• Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
• Efficient Algorithms for Checking Fast Termination in VASS
• 3-VASS Reachability is in EXPSPACE
• Condition length and complexity for the solution of polynomial systems
• On the Separability Problem of VASS Reachability Languages