Přehled o publikaci
2021
Deciding Polynomial Termination Complexity for VASS Programs
AJDARÓW, Michal and Antonín KUČERABasic information
Original name
Deciding Polynomial Termination Complexity for VASS Programs
Authors
AJDARÓW, Michal and Antonín KUČERA
Edition
Dagstuhl, Germany, 32nd International Conference on Concurrency Theory (CONCUR 2021), p. "30:1"-"30:15", 15 pp. 2021
Publisher
Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
Other information
Language
English
Type of outcome
Proceedings paper
Country of publisher
Germany
Confidentiality degree
is not subject to a state or trade secret
Publication form
electronic version available online
References:
Organization
Fakulta informatiky – Repository – Repository
ISBN
978-3-95977-203-7
ISSN
EID Scopus
2-s2.0-85115347017
Keywords (in Czech)
VASS; výpočetní složitost
Keywords in English
VASS; termination complexity
Links
GA21-24711S, research and development project. MUNI/A/1108/2020, interní kód Repo. MUNI/A/1549/2020, interní kód Repo.
Changed: 29/4/2022 03:09, RNDr. Daniel Jakubík
Abstract
V originále
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.
