Document Open Access Logo

Polynomial Vector Addition Systems With States

Author Jérôme Leroux

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2018.134.pdf
  • Filesize: 470 kB
  • 13 pages

Document Identifiers

Author Details

Jérôme Leroux
  • Univ.Bordeaux, CNRS, Bordeaux-INP, Talence, France

Funding

  • Leroux, Jérôme: The author was supported by the grant ANR-17-CE40-0028 of the French National Research Agency ANR (project BRAVAS)

Cite AsGet BibTex

Jérôme Leroux. Polynomial Vector Addition Systems With States. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 134:1-134:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.ICALP.2018.134

Abstract

The reachability problem for vector addition systems is one of the most difficult and central problems in theoretical computer science. The problem is known to be decidable, but despite intense investigation during the last four decades, the exact complexity is still open. For some sub-classes, the complexity of the reachability problem is known. Structurally bounded vector addition systems, the class of vector addition systems with finite reachability sets from any initial configuration, is one of those classes. In fact, the reachability problem was shown to be polynomial-space complete for that class by Praveen and Lodaya in 2008. Surprisingly, extending this property to vector addition systems with states is open. In fact, there exist vector addition systems with states that are structurally bounded but with Ackermannian large sets of reachable configurations. It follows that the reachability problem for that class is between exponential space and Ackermannian. In this paper we introduce the class of polynomial vector addition systems with states, defined as the class of vector addition systems with states with size of reachable configurations bounded polynomially in the size of the initial ones. We prove that the reachability problem for polynomial vector addition systems is exponential-space complete. Additionally, we show that we can decide in polynomial time if a vector addition system with states is polynomial. This characterization introduces the notion of iteration scheme with potential applications to the reachability problem for general vector addition systems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Vector additions system with states
  • Reachability problem
  • Formal verification
  • Infinite state system
  • Linear algebra
  • Kosaraju-Sullivan algorithm

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. I. Borosh and L. B. Treybig. Bounds on positive integral solutions of linear diophantine equations. Proc. Amer. Math. Soc., 55(2):299-304, 1976. URL: http://dx.doi.org/10.1090/S0002-9939-1976-0396605-3.
  2. E. Cohen and N. Megiddo. Strongly polynomial-time and NC algorithms for detecting cycles in dynamic graphs. In Proceedings of the Twenty-first Annual ACM Symposium on Theory of Computing, STOC '89, pages 523-534, New York, NY, USA, 1989. ACM. URL: http://dx.doi.org/10.1145/73007.73057.
  3. Javier Esparza. Decidability and complexity of Petri net problems - an introduction. In Advances in Petri Nets '98, volume 1491 of LNCS, pages 374-428. Springer, 1998. URL: http://dx.doi.org/10.1007/3-540-65306-6_20.
  4. Javier Esparza and Mogens Nielsen. Decidability issues for Petri nets - a survey. Bulletin of the EATCS, 52:244-262, 1994. Google Scholar
  5. Diego Figueira, Santiago Figueira, Sylvain Schmitz, and Philippe Schnoebelen. Ackermannian and primitive-recursive bounds with Dickson’s lemma. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada, pages 269-278. IEEE Computer Society, 2011. URL: http://dx.doi.org/10.1109/LICS.2011.39.
  6. John E. Hopcroft and Jean-Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci., 8:135-159, 1979. URL: http://dx.doi.org/10.1016/0304-3975(79)90041-0.
  7. S. Rao Kosaraju. Decidability of reachability in vector addition systems (preliminary version). In Harry R. Lewis, Barbara B. Simons, Walter A. Burkhard, and Lawrence H. Landweber, editors, Proceedings of the 14th Annual ACM Symposium on Theory of Computing, May 5-7, 1982, San Francisco, California, USA, pages 267-281. ACM, 1982. URL: http://dx.doi.org/10.1145/800070.802201.
  8. S. Rao Kosaraju and Gregory F. Sullivan. Detecting cycles in dynamic graphs in polynomial time (preliminary version). In Janos Simon, editor, Proceedings of the 20th Annual ACM Symposium on Theory of Computing, May 2-4, 1988, Chicago, Illinois, USA, pages 398-406. ACM, 1988. URL: http://dx.doi.org/10.1145/62212.62251.
  9. Jean-Luc Lambert. A structure to decide reachability in Petri nets. Theor. Comput. Sci., 99(1):79-104, 1992. URL: http://dx.doi.org/10.1016/0304-3975(92)90173-D.
  10. Jérôme Leroux. Vector addition systems reachability problem (A simpler solution). In Turing-100, volume 10 of EPiC Series in Computing, pages 214-228. EasyChair, 2012. Google Scholar
  11. Jérôme Leroux and Sylvain Schmitz. Demystifying reachability in vector addition systems. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 56-67. IEEE Computer Society, 2015. URL: http://dx.doi.org/10.1109/LICS.2015.16.
  12. R. J. Lipton. The reachability problem requires exponential space. Technical Report 63, Department of Computer Science, Yale University, 1976. Google Scholar
  13. Ernst W. Mayr. An algorithm for the general Petri net reachability problem. In Proceedings of the 13th Annual ACM Symposium on Theory of Computing, May 11-13, 1981, Milwaukee, Wisconsin, USA, pages 238-246. ACM, 1981. URL: http://dx.doi.org/10.1145/800076.802477.
  14. Ernst W. Mayr. An algorithm for the general Petri net reachability problem. SIAM J. Comput., 13(3):441-460, 1984. URL: http://dx.doi.org/10.1137/0213029.
  15. Ernst W. Mayr and Albert R. Meyer. The complexity of the finite containment problem for Petri nets. J. ACM, 28(3):561-576, 1981. URL: http://dx.doi.org/10.1145/322261.322271.
  16. Loic Pottier. Minimal solutions of linear diophantine systems: Bounds and algorithms. In Proceedings of the 4th International Conference on Rewriting Techniques and Applications, RTA '91, pages 162-173, London, UK, UK, 1991. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=647192.720494.
  17. M. Praveen and Kamal Lodaya. Analyzing reachability for some Petri nets with fast growing markings. Electr. Notes Theor. Comput. Sci., 223:215-237, 2008. URL: http://dx.doi.org/10.1016/j.entcs.2008.12.041.
  18. Charles Rackoff. The covering and boundedness problems for vector addition systems. Theor. Comput. Sci., 6:223-231, 1978. URL: http://dx.doi.org/10.1016/0304-3975(78)90036-1.
  19. Alexander Schrijver. Theory of Linear and Integer Programming. John Wiley and Sons, New York, 1987. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact