Deciding Polynomial Termination Complexity for VASS Programs

Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

AJDARÓW Michal KUČERA Antonín

Rok publikování 2021
Druh Článek ve sborníku
Konference 32nd International Conference on Concurrency Theory (CONCUR 2021)
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www Dagstuhl website
Doi http://dx.doi.org/10.4230/LIPIcs.CONCUR.2021.30
Klíčová slova VASS; termination complexity
Přiložené soubory
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.