Journal article
The reachability problem for two-dimensional vector addition systems with states
- 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.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Accepted manuscript, 1.0MB, Terms of use)
-
- Publisher copy:
- 10.1145/3464794
Authors
- Publisher:
- Association for Computing Machinery
- Journal:
- Journal of the ACM More from this journal
- Volume:
- 68
- Issue:
- 5
- Article number:
- 34
- Publication date:
- 2021-08-12
- Acceptance date:
- 2021-05-03
- DOI:
- EISSN:
-
1557-735X
- ISSN:
-
0004-5411
- Language:
-
English
- Keywords:
- Pubs id:
-
1174140
- Local pid:
-
pubs:1174140
- Deposit date:
-
2021-05-04
Terms of use
- Copyright holder:
- ACM, Inc.
- Copyright date:
- 2021
- Rights statement:
- Copyright © 2021 ACM, Inc.
- Notes:
-
This is the accepted manuscript version of the article. The final version is available from Association for Computing Machinery at https://doi.org/10.1145/3464794
If you are the owner of this record, you can report an update to it here: Report update to this record