The Reachability Problem for Two-Dimensional Vector Addition Systems with States

Blondin, Michael, Englert, Matthias, Finkel, Alain, Goeller, Stefan, Haase, Christoph, Lazic, Ranko, Mckenzie, Pierre and Totzke, Patrick ORCID: 0000-0001-5274-8190 (2021) The Reachability Problem for Two-Dimensional Vector Addition Systems with States. JOURNAL OF THE ACM, 68 (5). pp. 1-43.

Access the full-text of this item by clicking on the Open Access link.

Official URL: http://dx.doi.org/10.1145/3464794

Abstract

<jats:p>We prove that the reachability problem for two-dimensional vector addition systems with states is NL-complete or PSPACE-complete, depending on whether the numbers in the input are encoded in unary or binary. As a key underlying technical result, we show that, if a configuration is reachable, then there exists a witnessing path whose sequence of transitions is contained in a bounded language defined by a regular expression of pseudo-polynomially bounded length. This, in turn, enables us to prove that the lengths of minimal reachability witnesses are pseudo-polynomially bounded.</jats:p>

Item Type:	Article
Uncontrolled Keywords:	Vector addition systems with states, Petri nets, semi-linear sets, linear path schemes, reachability
Divisions:	Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User:	Symplectic Admin
Date Deposited:	15 Nov 2021 08:29
Last Modified:	18 Jan 2023 21:24
DOI:	10.1145/3464794
Open Access URL:	http://wrap.warwick.ac.uk/152742/
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3143102