Deciding Polynomial Termination Complexity for VASS Programs
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F21%3A00119194" target="_blank" >RIV/00216224:14330/21:00119194 - isvavai.cz</a>
Výsledek na webu
<a href="https://drops.dagstuhl.de/opus/volltexte/2021/14407" target="_blank" >https://drops.dagstuhl.de/opus/volltexte/2021/14407</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.4230/LIPIcs.CONCUR.2021.30" target="_blank" >10.4230/LIPIcs.CONCUR.2021.30</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Deciding Polynomial Termination Complexity for VASS Programs
Popis výsledku v původním jazyce
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.
Název v anglickém jazyce
Deciding Polynomial Termination Complexity for VASS Programs
Popis výsledku anglicky
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.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
—
OECD FORD obor
10200 - Computer and information sciences
Návaznosti výsledku
Projekt
<a href="/cs/project/GA21-24711S" target="_blank" >GA21-24711S: Efektivní analýza a optimalizace pravděpodobnostních systémů a her</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Ostatní
Rok uplatnění
2021
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
32nd International Conference on Concurrency Theory (CONCUR 2021)
ISBN
9783959772037
ISSN
1868-8969
e-ISSN
—
Počet stran výsledku
15
Strana od-do
„30:1“-„30:15“
Název nakladatele
Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
Místo vydání
Dagstuhl, Germany
Místo konání akce
Paris, France
Datum konání akce
23. 8. 2021
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—