Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete

Matthias  Englert; Ranko  Lazic; Patrick Totzke

doi:10.1145/2933575.2933577

Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete

Matthias Englert, Ranko Lazic, Patrick Totzke

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

Blondin et al. showed at LICS 2015 that two-dimensional vector addition systems with states have reachability witnesses of length exponential in the number of states and polynomial in the norm of vectors. The resulting guess-and-verify algorithm is optimal (PSPACE), but only if the input vectors are given in binary. We answer positively the main question left open by their work, namely establish that reachability witnesses of pseudo-polynomial length always exist. Hence, when the input vectors are given in unary, the improved guess-and-verify algorithm requires only logarithmic space.

Original language	English
Title of host publication	LICS '16 Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science
Place of Publication	New York, USA
Publisher	ACM
Pages	477-484
Number of pages	8
ISBN (Electronic)	978-1-4503-4391-6
DOIs	https://doi.org/10.1145/2933575.2933577
Publication status	Published - 5 Jul 2016
Event	31st Annual ACM/IEEE Symposium on Logic in Computer Science - New York City, United States Duration: 5 Jul 2016 → 8 Jul 2016 http://lics.siglog.org/lics16/

Conference

Conference	31st Annual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated title	LICS 2016
Country/Territory	United States
City	New York City
Period	5/07/16 → 8/07/16
Internet address	http://lics.siglog.org/lics16/

Access to Document

10.1145/2933575.2933577

ELT2016Accepted author manuscript, 349 KB

http://dl.acm.org/citation.cfm?doid=2933575.2933577

Cite this

@inproceedings{84bfc5745886494a841dfe878245fa67,

title = "Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete",

abstract = "Blondin et al. showed at LICS 2015 that two-dimensional vector addition systems with states have reachability witnesses of length exponential in the number of states and polynomial in the norm of vectors. The resulting guess-and-verify algorithm is optimal (PSPACE), but only if the input vectors are given in binary. We answer positively the main question left open by their work, namely establish that reachability witnesses of pseudo-polynomial length always exist. Hence, when the input vectors are given in unary, the improved guess-and-verify algorithm requires only logarithmic space.",

author = "Matthias Englert and Ranko Lazic and Patrick Totzke",

year = "2016",

month = jul,

day = "5",

doi = "10.1145/2933575.2933577",

language = "English",

pages = "477--484",

booktitle = "LICS '16 Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science",

publisher = "ACM",

note = "31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 ; Conference date: 05-07-2016 Through 08-07-2016",

url = "http://lics.siglog.org/lics16/",

}

Englert, M, Lazic, R & Totzke, P 2016, Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete. in LICS '16 Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. ACM, New York, USA, pp. 477-484, 31st Annual ACM/IEEE Symposium on Logic in Computer Science, New York City, New York, United States, 5/07/16. https://doi.org/10.1145/2933575.2933577

TY - GEN

T1 - Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete

AU - Englert, Matthias

AU - Lazic, Ranko

AU - Totzke, Patrick

PY - 2016/7/5

Y1 - 2016/7/5

N2 - Blondin et al. showed at LICS 2015 that two-dimensional vector addition systems with states have reachability witnesses of length exponential in the number of states and polynomial in the norm of vectors. The resulting guess-and-verify algorithm is optimal (PSPACE), but only if the input vectors are given in binary. We answer positively the main question left open by their work, namely establish that reachability witnesses of pseudo-polynomial length always exist. Hence, when the input vectors are given in unary, the improved guess-and-verify algorithm requires only logarithmic space.

AB - Blondin et al. showed at LICS 2015 that two-dimensional vector addition systems with states have reachability witnesses of length exponential in the number of states and polynomial in the norm of vectors. The resulting guess-and-verify algorithm is optimal (PSPACE), but only if the input vectors are given in binary. We answer positively the main question left open by their work, namely establish that reachability witnesses of pseudo-polynomial length always exist. Hence, when the input vectors are given in unary, the improved guess-and-verify algorithm requires only logarithmic space.

U2 - 10.1145/2933575.2933577

DO - 10.1145/2933575.2933577

M3 - Conference contribution

SP - 477

EP - 484

BT - LICS '16 Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science

PB - ACM

CY - New York, USA

T2 - 31st Annual ACM/IEEE Symposium on Logic in Computer Science

Y2 - 5 July 2016 through 8 July 2016

ER -

Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete

Abstract

Conference

Access to Document

Fingerprint

Cite this