Deciding Polynomial Termination Complexity for VASS Programs

D 2021

Deciding Polynomial Termination Complexity for VASS Programs

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

Basic information

Original name

Deciding Polynomial Termination Complexity for VASS Programs

Authors

AJDARÓW, Michal (203 Czech Republic, belonging to the institution) and Antonín KUČERA (203 Czech Republic, guarantor, belonging to the institution)

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

Stať ve sborníku

Field of Study

10200 1.2 Computer and information sciences

Country of publisher

Germany

Confidentiality degree

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

Publication form

electronic version available online

References:

Dagstuhl website

RIV identification code

RIV/00216224:14330/21:00119194

Organization unit

Faculty of Informatics

ISBN

978-3-95977-203-7

ISSN

DOI

http://dx.doi.org/10.4230/LIPIcs.CONCUR.2021.30

Keywords (in Czech)

VASS; výpočetní složitost

Keywords in English

VASS; termination complexity

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.

Links

GA21-24711S, research and development project

Name: Efektivní analýza a optimalizace pravděpodobnostních systémů a her (Acronym: Efektivní analýza a optimalizace pravděpodobnostní)

Investor: Czech Science Foundation

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

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

Investor: Masaryk University

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

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

Investor: Masaryk University

Files attached

LIPIcs-CONCUR-2021-30.pdf

Find similar documents

Citovat

AJDARÓW, Michal and 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, p. "30:1"-"30:15", 15 pp. ISBN 978-3-95977-203-7. Available from: https://dx.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 = {http://dx.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  - JOUR
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 and 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, p.~''30:1''-''30:15'', 15 pp. ISBN~978-3-95977-203-7. Available from: https://dx.doi.org/10.4230/LIPIcs.CONCUR.2021.30.

Detailed Information on Publication Record