Blondin, M, Englert, M, Finkel, A, Göller, S, Haase, C, Lazić, R, McKenzie, P and Totzke, P 
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.
ISSN 0004-5411, 1557-735X
Abstract
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.
| Item Type: | Article |
|---|---|
| Uncontrolled Keywords: | Vector addition systems with states, Petri nets, semi-linear sets, linear path schemes, reachability |
| Divisions: | Faculty of Science & Engineering > School of Electrical Engineering, Electronics and Computer Science |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 15 Nov 2021 08:29 |
| Last Modified: | 24 Jan 2026 03:12 |
| DOI: | 10.1145/3464794 |
| Open Access URL: | http://wrap.warwick.ac.uk/152742/ |
| Related Websites: | |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3143102 |
| Disclaimer: | The University of Liverpool is not responsible for content contained on other websites from links within repository metadata. Please contact us if you notice anything that appears incorrect or inappropriate. |
Altmetric
Altmetric