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 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:

URL

Organization

Fakulta informatiky – Repository – Repository

ISBN

978-3-95977-203-7

ISSN

DOI

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

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.
Displayed: 4/7/2025 14:49