D 2021

Deciding Polynomial Termination Complexity for VASS Programs

AJDARÓW, Michal a Antonín KUČERA

Základní údaje

Originální název

Deciding Polynomial Termination Complexity for VASS Programs

Autoři

AJDARÓW, Michal a Antonín KUČERA

Vydání

Dagstuhl, Germany, 32nd International Conference on Concurrency Theory (CONCUR 2021), od s. "30:1"-"30:15", 15 s. 2021

Nakladatel

Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Odkazy

Organizace

Fakulta informatiky – Masarykova univerzita – Repozitář

ISBN

978-3-95977-203-7

ISSN

EID Scopus

2-s2.0-85115347017

Klíčová slova česky

VASS; výpočetní složitost

Klíčová slova anglicky

VASS; termination complexity

Návaznosti

GA21-24711S, projekt VaV. MUNI/A/1108/2020, interní kód Repo. MUNI/A/1549/2020, interní kód Repo.
Změněno: 29. 4. 2022 03:09, RNDr. Daniel Jakubík

Anotace

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.

Přiložené soubory