Deciding Polynomial Termination Complexity for VASS Programs

Investor logo

Warning

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

AJDARÓW Michal KUČERA Antonín

Year of publication 2021
Type Article in Proceedings
Conference 32nd International Conference on Concurrency Theory (CONCUR 2021)
MU Faculty or unit

Faculty of Informatics

Citation
Web Dagstuhl website
Doi http://dx.doi.org/10.4230/LIPIcs.CONCUR.2021.30
Keywords VASS; termination complexity
Attached files
Description We show that for every fixed degree 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. 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 projects:

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