Document Open Access Logo

Affine Extensions of Integer Vector Addition Systems with States

Authors Michael Blondin , Christoph Haase , Filip Mazowiecki

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2018.14.pdf
  • Filesize: 0.64 MB
  • 17 pages

Document Identifiers

Author Details

Michael Blondin
  • Technische Universität München, Germany
Christoph Haase
  • University of Oxford, United Kingdom
Filip Mazowiecki
  • LaBRI, Université de Bordeaux, France

Funding

  • Blondin, Michael: Supported by the Fonds de recherche du Québec – Nature et technologies (FRQNT).
  • Mazowiecki, Filip: This study has been carried out with financial support from the French State, managed by the French National Research Agency (ANR) in the frame of the "Investments for the future" Programme IdEx Bordeaux (ANR-10-IDEX-03-02).

Cite AsGet BibTex

Michael Blondin, Christoph Haase, and Filip Mazowiecki. Affine Extensions of Integer Vector Addition Systems with States. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CONCUR.2018.14

Abstract

We study the reachability problem for affine Z-VASS, which are integer vector addition systems with states in which transitions perform affine transformations on the counters. This problem is easily seen to be undecidable in general, and we therefore restrict ourselves to affine Z-VASS with the finite-monoid property (afmp-Z-VASS). The latter have the property that the monoid generated by the matrices appearing in their affine transformations is finite. The class of afmp-Z-VASS encompasses classical operations of counter machines such as resets, permutations, transfers and copies. We show that reachability in an afmp-Z-VASS reduces to reachability in a Z-VASS whose control-states grow polynomially in the size of the matrix monoid. Our construction shows that reachability relations of afmp-Z-VASS are semilinear, and in particular enables us to show that reachability in Z-VASS with transfers and Z-VASS with copies is PSPACE-complete.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Complexity classes
Keywords
  • Vector addition systems
  • affine transformations
  • reachability
  • semilinear sets
  • computational complexity

Metrics

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

References

  1. Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. General decidability theorems for infinite-state systems. In Proc. 11^th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 313-321, 1996. URL: http://dx.doi.org/10.1109/LICS.1996.561359.
  2. Parosh Aziz Abdulla and Giorgio Delzanno. Parameterized verification. International Journal on Software Tools for Technology Transfer, 18(5):469-473, 2016. URL: http://dx.doi.org/10.1007/s10009-016-0424-3.
  3. Rajeev Alur, Adam Freilich, and Mukund Raghothaman. Regular combinators for string transformations. In Proc. Joint Meeting of the 23^rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29^th ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 9:1-9:10, 2014. URL: http://dx.doi.org/10.1145/2603088.2603151.
  4. Rajeev Alur and Mukund Raghothaman. Decision problems for additive regular functions. In Proc. 40^th International Colloquium on Automata, Languages, and Programming (ICALP), pages 37-48, 2013. URL: http://dx.doi.org/10.1007/978-3-642-39212-2_7.
  5. Toshiro Araki and Tadao Kasami. Some decision problems related to the reachability problem for Petri nets. Theoretical Computer Science, 3(1):85-104, 1976. URL: http://dx.doi.org/10.1016/0304-3975(76)90067-0.
  6. Konstantinos Athanasiou, Peizun Liu, and Thomas Wahl. Unbounded-thread program verification using thread-state equations. In Proc. 8^th International Joint Conference on Automated Reasoning (IJCAR), pages 516-531, 2016. URL: http://dx.doi.org/10.1007/978-3-319-40229-1_35.
  7. Michael Blondin, Alain Finkel, Stefan Göller, Christoph Haase, and Pierre McKenzie. Reachability in two-dimensional vector addition systems with states is PSPACE-complete. In Proc. 30^th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 32-43, 2015. URL: http://dx.doi.org/10.1109/LICS.2015.14.
  8. Michael Blondin and Christoph Haase. Logics for continuous reachability in Petri nets and vector addition systems with states. In Proc. 32^nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12, 2017. URL: http://dx.doi.org/10.1109/LICS.2017.8005068.
  9. Bernard Boigelot. Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, Université de Liège, Belgium, 1998. Google Scholar
  10. Rémi Bonnet. Theory of Well-Structured Transition Systems and Extended Vector-Addition Systems. PhD thesis, École normale supérieure de Cachan, France, 2013. Google Scholar
  11. I. Borosh and L. B. Treybig. Bounds on positive integral solutions of linear diophantine equations. Proceedings of the American Mathematical Society, 55(2):299-304, 1976. URL: http://dx.doi.org/10.2307/2041711.
  12. Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. Bounded Parikh automata. International Journal of Foundations of Computer Science, 23(8):1691-1710, 2012. URL: http://dx.doi.org/10.1142/S0129054112400709.
  13. Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. Unambiguous constrained automata. International Journal of Foundations of Computer Science, 24(7):1099-1116, 2013. URL: http://dx.doi.org/10.1142/S0129054113400339.
  14. Dmitry Chistikov and Christoph Haase. The taming of the semi-linear set. In Proc. 43^rd International Colloquium on Automata, Languages, and Programming (ICALP), pages 128:1-128:13, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.ICALP.2016.128.
  15. Giorgio Delzanno. A unified view of parameterized verification of abstract models of broadcast communication. International Journal on Software Tools for Technology Transfer, 18(5):475-493, 2016. URL: http://dx.doi.org/10.1007/s10009-016-0412-7.
  16. Catherine Dufourd, Alain Finkel, and Philippe Schnoebelen. Reset nets between decidability and undecidability. In Proc. 25^th International Colloquium on Automata, Languages and Programming (ICALP), pages 103-115, 1998. URL: http://dx.doi.org/10.1007/BFb0055044.
  17. E. Allen Emerson and Kedar S. Namjoshi. On model checking for non-deterministic infinite-state systems. In Proc. 13^th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 70-80, 1998. URL: http://dx.doi.org/10.1109/LICS.1998.705644.
  18. Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp J. Meyer, and Filip Niksic. An SMT-based approach to coverability analysis. In Proc. 26^th International Conference on Computer Aided Verification (CAV), pages 603-619, 2014. URL: http://dx.doi.org/10.1007/978-3-319-08867-9_40.
  19. Diego Figueira, Santiago Figueira, Sylvain Schmitz, and Philippe Schnoebelen. Ackermannian and primitive-recursive bounds with Dickson’s lemma. In Proc. 26^th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 269-278, 2011. URL: http://dx.doi.org/10.1109/LICS.2011.39.
  20. Alain Finkel and Jérôme Leroux. How to compose Presburger-accelerations: Applications to broadcast protocols. In Proc. 22^nd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pages 145-156, 2002. URL: http://dx.doi.org/10.1007/3-540-36206-1_14.
  21. Christoph Haase and Simon Halfon. Integer vector addition systems with states. In Proc. 8^th International Workshop on Reachability Problems (RP), pages 112-124, 2014. URL: http://dx.doi.org/10.1007/978-3-319-11439-2_9.
  22. John E. Hopcroft and Jean-Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theoretical Computer Science, 8:135-159, 1979. URL: http://dx.doi.org/10.1016/0304-3975(79)90041-0.
  23. John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979. Google Scholar
  24. Radu Iosif and Arnaud Sangnier. How hard is it to verify flat affine counter systems with the finite monoid property? In Proc. 14^th International Symposium on Automated Technology for Verification and Analysis (ATVA), pages 89-105, 2016. URL: http://dx.doi.org/10.1007/978-3-319-46520-3_6.
  25. Alexander Kaiser, Daniel Kroening, and Thomas Wahl. A widening approach to multithreaded program verification. ACM Transactions on Programming Languages and Systems, 36(4):14:1-14:29, 2014. URL: http://dx.doi.org/10.1145/2629608.
  26. Richard M. Karp and Raymond E. Miller. Parallel program schemata. Journal of Computer and System Sciences, 3(2):147-195, 1969. URL: http://dx.doi.org/10.1016/S0022-0000(69)80011-5.
  27. S. Rao Kosaraju. Decidability of reachability in vector addition systems (preliminary version). In Proc. 14^th Annual ACM Symposium on Theory of Computing (STOC), pages 267-281, 1982. URL: http://dx.doi.org/10.1145/800070.802201.
  28. James Kuzmanovich and Andrey Pavlichenkov. Finite groups of matrices whose entries are integers. The American Mathematical Monthly, 109(2):173-186, 2002. URL: http://dx.doi.org/10.2307/2695329.
  29. Jérôme Leroux. Vector addition systems reachability problem (a simpler solution). In The Alan Turing Centenary Conference, pages 214-228, 2012. Google Scholar
  30. Richard J. Lipton. The reachability problem requires exponential space. Technical Report 63, Department of Computer Science, Yale University, 1976. Google Scholar
  31. Arnaldo Mandel and Imre Simon. On finite semigroups of matrices. Theoretical Computer Science, 5(2):101-111, 1977. URL: http://dx.doi.org/10.1016/0304-3975(77)90001-9.
  32. Ernst W. Mayr. An algorithm for the general Petri net reachability problem. SIAM Journal on Computing, 13(3):441-460, 1984. URL: http://dx.doi.org/10.1137/0213029.
  33. Marvin Lee Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, 1967. Google Scholar
  34. Mojżesz Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Comptes Rendus du I^er Congrès des mathématiciens des pays slaves, pages 192-201, 1929. Google Scholar
  35. Charles Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6:223-231, 1978. URL: http://dx.doi.org/10.1016/0304-3975(78)90036-1.
  36. Julien Reichert. Reachability games with counters: decidability and algorithms. PhD thesis, École normale supérieure de Cachan, France, 2015. Google Scholar
  37. Klaus Reinhardt. Reachability in Petri nets with inhibitor arcs. Electronic Notes in Theoretical Computer Science, 223:239-264, 2008. URL: http://dx.doi.org/10.1016/j.entcs.2008.12.042.
  38. Philippe Schnoebelen. Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets. In Proc. 35^th International Symposium Mathematical Foundations of Computer Science (MFCS), pages 616-628, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15155-2_54.
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