research-article

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

Authors:

Matthias Englert,

Ranko Lazić,

Patrick TotzkeAuthors Info & Claims

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

Pages 477 - 484

https://doi.org/10.1145/2933575.2933577

Published: 05 July 2016 Publication History

Get Access

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.

References

[1]

M. Blondin, A. Finkel, S. Göller, C. Haase, and P. McKenzie. Reachability in two-dimensional vector addition systems with states is PSPACEcomplete. In LICS, pages 32--43. IEEE, 2015.

Digital Library

Google Scholar

[2]

E. Cardoza, R. J. Lipton, and A. R. Meyer. Exponential space complete problems for Petri nets and commutative semigroups: Preliminary report. In STOC, pages 50--54. ACM, 1976.

Digital Library

Google Scholar

[3]

S. M. German and A. P. Sistla. Reasoning about systems with many processes. J. ACM, 39(3):675--735, 1992.

Digital Library

Google Scholar

[4]

C. Haase, S. Kreutzer, J. Ouaknine, and J. Worrell. Reachability in succinct and parametric one-counter automata. In CONCUR, volume 5710 of LNCS, pages 369--383. Springer, 2009. 25.

Digital Library

Google Scholar

[5]

J. Leroux and S. Schmitz. Demystifying reachability in vector addition systems. In LICS, pages 56--67. IEEE, 2015.

Digital Library

Google Scholar

[6]

R. J. Lipton. The reachability problem requires exponential space. Technical Report 62, Yale University, 1976. URL http://cpsc.yale. edu/sites/default/files/files/tr63.pdf.

Google Scholar

[7]

L. E. Rosier and H. Yen. A multiparameter analysis of the boundedness problem for vector addition systems. J. Comput. Syst. Sci., 32(1):105--135, 1986.

Digital Library

Google Scholar

[8]

S. Schmitz. Automata column: The complexity of reachability in vector addition systems. ACM SIGLOG News, 3(1), 2016. URL http://siglog.hosting.acm.org/wp-content/uploads/2016/01/siglog_news_7.pdf.

Digital Library

Google Scholar

[9]

L. G. Valiant and M. S. Paterson. Deterministic one-counter automata. J. Comput. Syst. Sci., 10(3):340--350, 1975.

Digital Library

Google Scholar

Cited By

View all

Li YZhang QReps T(2023)Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear ProgrammingProceedings of the ACM on Programming Languages10.1145/35712287:POPL(1003-1026)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1145/3571228
Mazowiecki FSinclair-Banks HWęgrzycki K(2023)Coverability in 2-VASS with One Unary Counter is in NPFoundations of Software Science and Computation Structures10.1007/978-3-031-30829-1_10(196-217)Online publication date: 21-Apr-2023
https://doi.org/10.1007/978-3-031-30829-1_10
Pavlogiannis A(2022)CFL/Dyck ReachabilityACM SIGLOG News10.1145/3583660.35836649:4(5-25)Online publication date: 1-Oct-2022
https://dl.acm.org/doi/10.1145/3583660.3583664
Show More Cited By

Recommendations

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 ...
Binary Reachability of Timed-register Pushdown Automata and Branching Vector Addition Systems

Timed-register pushdown automata constitute a very expressive class of automata, whose transitions may involve state, input, and top-of-stack timed registers with unbounded differences. They strictly subsume pushdown timed automata of Bouajjani et al., ...
Timed pushdown automata and branching vector addition systems
LICS '17: Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science

We prove that non-emptiness of timed register pushdown automata is decidable in doubly exponential time. This is a very expressive class of automata, whose transitions may involve state and top-of-stack clocks with unbounded differences. It strictly ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

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

July 2016

901 pages

ISBN:9781450343916

DOI:10.1145/2933575

Conference Chair:
Eric Koskinen,
General Chair:
Martin Grohe,
Program Chair:
Natarajan Shankar

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 July 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article
Research
Refereed limited

Funding Sources

EPSC
EPSRC

Conference

LICS '16

Sponsor:

SIGLOG
EACSL
IEEE-CS\DATC

LICS '16: 31st Annual ACM/IEEE Symposium on Logic in Computer Science

July 5 - 8, 2016

NY, New York, USA

Acceptance Rates

Overall Acceptance Rate 215 of 622 submissions, 35%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
101
Total Downloads

Downloads (Last 12 months)15
Downloads (Last 6 weeks)2

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Li YZhang QReps T(2023)Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear ProgrammingProceedings of the ACM on Programming Languages10.1145/35712287:POPL(1003-1026)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1145/3571228
Mazowiecki FSinclair-Banks HWęgrzycki K(2023)Coverability in 2-VASS with One Unary Counter is in NPFoundations of Software Science and Computation Structures10.1007/978-3-031-30829-1_10(196-217)Online publication date: 21-Apr-2023
https://doi.org/10.1007/978-3-031-30829-1_10
Pavlogiannis A(2022)CFL/Dyck ReachabilityACM SIGLOG News10.1145/3583660.35836649:4(5-25)Online publication date: 1-Oct-2022
https://dl.acm.org/doi/10.1145/3583660.3583664
Czerwinski WOrlikowski L(2022)Lower Bounds for the Reachability Problem in Fixed Dimensional VASSesProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3533357(1-12)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3533357
Kjelstrøm APavlogiannis A(2022)The decidability and complexity of interleaved bidirected Dyck reachabilityProceedings of the ACM on Programming Languages10.1145/34986736:POPL(1-26)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498673
Czerwinski WOrlikowski L(2022)Reachability in Vector Addition Systems is Ackermann-complete2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS)10.1109/FOCS52979.2021.00120(1229-1240)Online publication date: Feb-2022
https://doi.org/10.1109/FOCS52979.2021.00120
Blondin MEnglert MFinkel AGÖller SHaase CLazić RMckenzie PTotzke P(2021)The Reachability Problem for Two-Dimensional Vector Addition Systems with StatesJournal of the ACM10.1145/346479468:5(1-43)Online publication date: 12-Aug-2021
https://dl.acm.org/doi/10.1145/3464794
Cojocaru L(2021)Towards the Complexity of Petri Nets and One Counter Machines via Coordinated Table Selective Substitution Systems2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)10.1109/SYNASC54541.2021.00042(200-207)Online publication date: Dec-2021
https://doi.org/10.1109/SYNASC54541.2021.00042
Leroux J(2021)Flat Petri Nets (Invited Talk)Application and Theory of Petri Nets and Concurrency10.1007/978-3-030-76983-3_2(17-30)Online publication date: 16-Jun-2021
https://doi.org/10.1007/978-3-030-76983-3_2
Leroux JSchmitz SBouyer P(2019)Reachability in vector addition systems is primitive-recursive in fixed dimensionProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470202(1-13)Online publication date: 24-Jun-2019
https://dl.acm.org/doi/10.5555/3470152.3470202
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Recommendations

The Reachability Problem for Two-Dimensional Vector Addition Systems with States

Binary Reachability of Timed-register Pushdown Automata and Branching Vector Addition Systems

Timed pushdown automata and branching vector addition systems