Name
Abstract | ||
|---|---|---|
AbstractWe 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. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.1145/3464794 | Journal of the ACM |
Keywords | DocType | Volume |
Vector addition systems with states, Petri nets, semi-linear sets, linear path schemes, reachability | Journal | 68 |
Issue | ISSN | Citations |
5 | 0004-5411 | 0 |
PageRank | References | Authors |
0.34 | 0 | 8 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Michael Blondin | 1 | 27 | 9.06 |
| Matthias Englert | 2 | 266 | 18.69 |
| Alain Finkel | 3 | 0 | 0.34 |
| Stefan Göller | 4 | 0 | 0.34 |
| Christoph Haase | 5 | 0 | 1.01 |
| Ranko Lazic | 6 | 306 | 23.95 |
| Pierre McKenzie | 7 | 188 | 15.94 |
| Patrick Totzke | 8 | 38 | 8.52 |