Article

Reachability in Two-Dimensional Vector Addition Systems with States Is PSPACE-Complete

Authors:

Michael Blondin,

Christoph Haase,

Pierre McKenzieAuthors Info & Claims

LICS '15: Proceedings of the 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

Pages 32 - 43

https://doi.org/10.1109/LICS.2015.14

Published: 06 July 2015 Publication History

First page of PDF

References

[1]

T. Ball, S. Chaki, and S. Rajamani, "Parameterized verification of multithreaded software libraries," in Tools and Algorithms for the Construction and Analysis of Systems, ser. Lecture Notes in Computer Science, vol. 2031. Springer, 2001, pp. 158-173.

Digital Library

[2]

T. Chan, "The boundedness problem for three-dimensional vector addition systems with states," Information Processing Letters, vol. 26, no. 6, pp. 287-289, 1988.

Digital Library

[3]

J. Fearnley and M. Jurdzinski, "Reachability in two-clock timed automata is PSPACE-complete," in Automata, Languages, and Programming, ser. Lecture Notes in Computer Science, vol. 7966. Springer, 2013, pp. 212-223.

Digital Library

[4]

S. M. German and A. P. Sistla, "Reasoning about systems with many processes," Journal of the ACM, vol. 39, no. 3, pp. 675-735, Jul. 1992.

Digital Library

[5]

C. Haase, S. Kreutzer, J. Ouaknine, and J. Worrell, "Reachability in succinct and parametric one-counter automata," in CONCUR 2009 - Concurrency Theory, ser. Lecture Notes in Computer Science, vol. 5710. Springer, 2009, pp. 369-383.

Digital Library

[6]

C. Haase, "On the complexity of model checking counter automata," Ph.D. dissertation, University of Oxford, 2012.

[7]

C. Haase and S. Halfon, "Integer vector addition systems with states," in Reachability Problems - 8th International Workshop, ser. Lecture Notes in Computer Science, vol. 8762. Springer, 2014, pp. 112-124.

[8]

M. Heiner, D. Gilbert, and R. Donaldson, "Petri nets for systems and synthetic biology," in Formal Methods for Computational Systems Biology, 2008, pp. 215-264.

Digital Library

[9]

J. Hopcroft and J.-J. Pansiot, "On the reachability problem for 5- dimensional vector addition systems," Theoretical Computer Science, vol. 8, no. 2, pp. 135-159, 1979.

[10]

R. R. Howell, L. E. Rosier, D. T. Huynh, and H.-C. Yen, "Some complexity bounds for problems concerning finite and 2-dimensional vector addition systems with states," Theoretical Computer Science, vol. 46, no. 3, pp. 107-140, 1986.

Digital Library

[11]

S. R. Kosaraju, "Decidability of reachability in vector addition systems (preliminary version)," in Proceedings of the 14th annual ACM symposium on Theory of computing. ACM, 1982, pp. 267-281.

Digital Library

[12]

J.-L. Lambert, "A structure to decide reachability in Petri nets," Theoretical Computer Science, vol. 99, no. 1, pp. 79-104, 1992.

Digital Library

[13]

J. Leroux and S. Schmitz, "Reachability in vector addition systems demystified," in Proceedings of the 30th Annual ACM/IEEE Symposium on Logic In Computer Science. ACM, 2015, to appear.

Digital Library

[14]

J. Leroux and G. Sutre, "On flatness for 2-dimensional vector addition systems with states," in CONCUR 2004 - Concurrency Theory, ser. Lecture Notes in Computer Science, vol. 3170. Springer, 2004, pp. 402-416.

[15]

J. Leroux, "Vector addition systems reachability problem (a simpler solution)," in Turing-100, ser. EPiC Series, vol. 10. EasyChair, 2012, pp. 214-228.

[16]

J. Leroux, "The general vector addition system reachability problem by presburger inductive invariants," in Proceedings of the 24th Annual IEEE Symposium on Symposium on Logic in Computer Science. IEEE, 2009, pp. 4-13.

Digital Library

[17]

R. J. Lipton, "The reachability problem is exponential-space-hard," Department of Computer Science, Yale University, Tech. Rep. 62, 1976.

[18]

E. W. Mayr, "An algorithm for the general Petri net reachability problem," in Proceedings of the 13th Annual ACM Symposium on Theory of Computing. ACM, 1981, pp. 238-246.

Digital Library

[19]

C. A. Petri, Kommunikation mit Automaten. Bonn: Institut für Instrumentelle Mathematik, Schriften des IIM Nr. 2, 1962.

[20]

L. Pottier, "Minimal solutions of linear Diophantine systems : bounds and algorithms," in Rewriting Techniques and Applications, ser. Lecture Notes in Computer Science, vol. 488. Springer, 1991, pp. 162-173.

Digital Library

[21]

V. Reddy, M. Liebman, and M. Mavrovouniotis, "Qualitative analysis of biochemical reaction systems," Computers in biology and medicine, vol. 26, no. 1, pp. 9-24, 1996.

[22]

L. E. Rosier and H.-C. Yen, "A multiparameter analysis of the boundedness problem for vector addition systems," Journal of Computer and System Sciences, vol. 32, no. 1, pp. 105-135, 1986.

Digital Library

[23]

G. S. Sacerdote and R. L. Tenney, "The decidability of the reachability problem for vector addition systems (preliminary version)," in Proceedings of the 9th annual ACM symposium on Theory of computing. ACM, 1977, pp. 61-76.

Digital Library

[24]

A. Schrijver, Theory of linear and integer programming. John Wiley & Sons, 1998.

Digital Library

[25]

A. W. To, "Model checking infinite-state systems: generic and specific approaches," Ph.D. dissertation, University of Edinburgh, 2010.

[26]

L. G. Valiant and M. Paterson, "Deterministic one-counter automata," Journal of Computer and System Sciences, vol. 10, no. 3, pp. 340-350, 1975.

Digital Library

[27]

W. van der Aalst, "The application of Petri nets to workflow management," Journal of circuits, systems, and computers, vol. 8, no. 1, pp. 21-66, 1998.

Cited By

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
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
Blondin M(2020)The ABCs of petri net reachability relaxationsACM SIGLOG News10.1145/3436980.34369847:3(29-43)Online publication date: 16-Nov-2020
https://dl.acm.org/doi/10.1145/3436980.3436984
Show More Cited By

Reachability in Two-Dimensional Vector Addition Systems with States Is PSPACE-Complete
1. Theory of computation

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 ...
Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete
LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science

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 ...
Robustness of PSPACE-complete sets

We study the robustness of complete languages in PSPACE and prove that they are robust against P-selective sparse sets. Earlier similar results are known for EXP-complete sets [H. Buhrman, A. Hoene, L. Torenvliet, Splittings, robustness, and structure ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

LICS '15: Proceedings of the 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

July 2015

776 pages

ISBN:9781479988754

Sponsors

In-Cooperation

EACSL: European Association for Computer Science Logic

Publisher

IEEE Computer Society

United States

Publication History

Published: 06 July 2015

Check for updates

Qualifiers

Article

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
52
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)1

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

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
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
Blondin M(2020)The ABCs of petri net reachability relaxationsACM SIGLOG News10.1145/3436980.34369847:3(29-43)Online publication date: 16-Nov-2020
https://dl.acm.org/doi/10.1145/3436980.3436984
Czerwiński WLasota SLazić RLeroux JMazowiecki F(2020)The Reachability Problem for Petri Nets Is Not ElementaryJournal of the ACM10.1145/342282268:1(1-28)Online publication date: 22-Dec-2020
https://dl.acm.org/doi/10.1145/3422822
Niskanen RPotapov IReichert J(2020)On decidability and complexity of low-dimensional robot gamesJournal of Computer and System Sciences10.1016/j.jcss.2019.08.003107:C(124-141)Online publication date: 1-Feb-2020
https://dl.acm.org/doi/10.1016/j.jcss.2019.08.003
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
Belardinelli FDemri SElkind EVeloso MAgmon NTaylor M(2019)Resource-bounded ATLProceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems10.5555/3306127.3331694(206-214)Online publication date: 8-May-2019
https://dl.acm.org/doi/10.5555/3306127.3331694
Czerwiński WLasota SAceto LIngólfsdóttir A(2017)Regular separability of one counter automataProceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3329995.3330014(1-12)Online publication date: 20-Jun-2017
https://dl.acm.org/doi/10.5555/3329995.3330014
Hofman PLeroux JTotzke PAceto LIngólfsdóttir A(2017)Linear combinations of unordered data vectorsProceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3329995.3330000(1-11)Online publication date: 20-Jun-2017
https://dl.acm.org/doi/10.5555/3329995.3330000
Englert MLazić RTotzke PKoskinen EGrohe MShankar N(2016)Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-CompleteProceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/2933575.2933577(477-484)Online publication date: 5-Jul-2016
https://dl.acm.org/doi/10.1145/2933575.2933577
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.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents