Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH scholarly article en Ajdarów, Michal; Kučera, Antonín https://www.dagstuhl.de/lipics License: Creative Commons Attribution 4.0 license (CC BY 4.0)
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-144076
URL:

;

Deciding Polynomial Termination Complexity for VASS Programs

pdf-format:


Abstract

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.

BibTeX - Entry

@InProceedings{ajdarow_et_al:LIPIcs.CONCUR.2021.30,
  author =	{Ajdar\'{o}w, Michal and Ku\v{c}era, Anton{\'\i}n},
  title =	{{Deciding Polynomial Termination Complexity for VASS Programs}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{30:1--30:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14407},
  URN =		{urn:nbn:de:0030-drops-144076},
  doi =		{10.4230/LIPIcs.CONCUR.2021.30},
  annote =	{Keywords: Termination complexity, vector addition systems}
}

Keywords: Termination complexity, vector addition systems
Seminar: 32nd International Conference on Concurrency Theory (CONCUR 2021)
Issue date: 2021
Date of publication: 13.08.2021


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI