License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2018.134
URN: urn:nbn:de:0030-drops-91387
URL: http://drops.dagstuhl.de/opus/volltexte/2018/9138/
Go to the corresponding LIPIcs Volume Portal


Leroux, Jérôme

Polynomial Vector Addition Systems With States

pdf-format:
LIPIcs-ICALP-2018-134.pdf (0.5 MB)


Abstract

The reachability problem for vector addition systems is one of the most difficult and central problems in theoretical computer science. The problem is known to be decidable, but despite intense investigation during the last four decades, the exact complexity is still open. For some sub-classes, the complexity of the reachability problem is known. Structurally bounded vector addition systems, the class of vector addition systems with finite reachability sets from any initial configuration, is one of those classes. In fact, the reachability problem was shown to be polynomial-space complete for that class by Praveen and Lodaya in 2008. Surprisingly, extending this property to vector addition systems with states is open. In fact, there exist vector addition systems with states that are structurally bounded but with Ackermannian large sets of reachable configurations. It follows that the reachability problem for that class is between exponential space and Ackermannian. In this paper we introduce the class of polynomial vector addition systems with states, defined as the class of vector addition systems with states with size of reachable configurations bounded polynomially in the size of the initial ones. We prove that the reachability problem for polynomial vector addition systems is exponential-space complete. Additionally, we show that we can decide in polynomial time if a vector addition system with states is polynomial. This characterization introduces the notion of iteration scheme with potential applications to the reachability problem for general vector addition systems.

BibTeX - Entry

@InProceedings{leroux:LIPIcs:2018:9138,
  author =	{J{\'e}r{\^o}me Leroux},
  title =	{{Polynomial Vector Addition Systems With States}},
  booktitle =	{45th International Colloquium on Automata, Languages, and  Programming (ICALP 2018)},
  pages =	{134:1--134:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-076-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{107},
  editor =	{Ioannis Chatzigiannakis and Christos Kaklamanis and D{\'a}niel Marx and Donald Sannella},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9138},
  URN =		{urn:nbn:de:0030-drops-91387},
  doi =		{10.4230/LIPIcs.ICALP.2018.134},
  annote =	{Keywords: Vector additions system with states, Reachability problem, Formal verification, Infinite state system, Linear algebra, Kosaraju-Sullivan algorithm}
}

Keywords: Vector additions system with states, Reachability problem, Formal verification, Infinite state system, Linear algebra, Kosaraju-Sullivan algorithm
Seminar: 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)
Issue Date: 2018
Date of publication: 29.06.2018


DROPS-Home | Imprint | Privacy Published by LZI