Deciding Polynomial Termination Complexity for VASS Programs

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

Obor

10200 1.2 Computer and information sciences

Stát vydavatele

Německo

Utajení

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

Forma vydání

elektronická verze "online"

Odkazy

Dagstuhl website

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/21:00119194

Organizační jednotka

Fakulta informatiky

ISBN

978-3-95977-203-7

ISSN

Klíčová slova česky

VASS; výpočetní složitost

Klíčová slova anglicky

VASS; termination complexity

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 13. 4. 2026 11:54, Mgr. Petra Trembecká, Ph.D.

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.

Návaznosti

GA21-24711S, projekt VaV

Název: Efektivní analýza a optimalizace pravděpodobnostních systémů a her (Akronym: Efektivní analýza a optimalizace pravděpodobnostní)

Investor: Grantová agentura ČR, Efektivní analýza a optimalizace pravděpodobnostních systémů a her

MUNI/A/1108/2020, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace X. (Akronym: SV-FI MAV X.)

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace X.

MUNI/A/1549/2020, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 21 (Akronym: SKOMU)

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 21

Přiložené soubory

LIPIcs-CONCUR-2021-30.pdf

Citovat

AJDARÓW, Michal a Antonín KUČERA. Deciding Polynomial Termination Complexity for VASS Programs. Online. In Haddad, Serge and Varacca, Daniele. 32nd International Conference on Concurrency Theory (CONCUR 2021). Dagstuhl, Germany: Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, 2021, s. "30:1"-"30:15", 15 s. ISBN 978-3-95977-203-7. Dostupné z: https://doi.org/10.4230/LIPIcs.CONCUR.2021.30.

@inproceedings{1790538,
   author = {Ajdarów, Michal and Kučera, Antonín},
   address = {Dagstuhl, Germany},
   booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
   doi = {https://doi.org/10.4230/LIPIcs.CONCUR.2021.30},
   editor = {Haddad, Serge and Varacca, Daniele},
   keywords = {VASS; termination complexity},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Dagstuhl, Germany},
   isbn = {978-3-95977-203-7},
   pages = {"30:1"-"30:15"},
   publisher = {Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik},
   title = {Deciding Polynomial Termination Complexity for VASS Programs},
   url = {https://drops.dagstuhl.de/opus/volltexte/2021/14407},
   year = {2021}
}

TY  - CONF
ID  - 1790538
AU  - Ajdarów, Michal - Kučera, Antonín
PY  - 2021
TI  - Deciding Polynomial Termination Complexity for VASS Programs
PB  - Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
CY  - Dagstuhl, Germany
SN  - 9783959772037
KW  - VASS
KW  - termination complexity
UR  - https://drops.dagstuhl.de/opus/volltexte/2021/14407
N2  - 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.
ER  -

AJDARÓW, Michal a Antonín KUČERA. Deciding Polynomial Termination Complexity for VASS Programs. Online. In Haddad, Serge and Varacca, Daniele. \textit{32nd International Conference on Concurrency Theory (CONCUR 2021)}. Dagstuhl, Germany: Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, 2021, s.~''30:1''-''30:15'', 15 s. ISBN~978-3-95977-203-7. Dostupné z: https://doi.org/10.4230/LIPIcs.CONCUR.2021.30.

Přehled o publikaci