The reachability problem for two-dimensional vector addition systems with states

The reachability problem for two-dimensional vector addition systems with states

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 th...

Täydet tiedot

Bibliografiset tiedot
Päätekijät: Blondin, M, Englert, M, Finkel, A, Göller, S, Haase, C, Lazic, R, McKenzie, P, Totzke, P
Aineistotyyppi: Journal article
Kieli:English
Julkaistu: Association for Computing Machinery 2021
Kuvaus
Yhteenveto: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.

Samankaltaisia teoksia