Finkel Was Right: Counter-Examples to Several Conjectures on Variants of Vector Addition Systems (Invited Talk)

Author Ranko Lazić

Thumbnail PDF


  • Filesize: 280 kB
  • 2 pages

Document Identifiers

Author Details

Ranko Lazić
  • DIMAP, Department of Computer Science, University of Warwick, UK


This presentation is based on joint work with Wojciech Czerwiński, Sławomir Lasota, Jérôme Leroux and Filip Mazowiecki. I also thank Matthias Englert for inspiring conversations about these variants of vector addition systems.

Cite AsGet BibTex

Ranko Lazić. Finkel Was Right: Counter-Examples to Several Conjectures on Variants of Vector Addition Systems (Invited Talk). In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Studying one-dimensional grammar vector addition systems has long been advocated by Alain Finkel. In this presentation, we shall see how research on those systems has led to the recent breakthrough tower lower bound for the reachability problem on vector addition systems, obtained by Czerwiński et al. In fact, we shall look at how appropriate modifications of an underlying technical construction can lead to counter-examples to several conjectures on one-dimensional grammar vector addition systems, fixed-dimensional vector addition systems, and fixed-dimensional flat vector addition systems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Verification by model checking
  • Theory of computation → Program reasoning
  • Petri nets
  • vector addition systems
  • reachability


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


  1. Matthias Englert, Ranko Lazić, and Patrick Totzke. Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete. In LICS, pages 477-484. ACM, 2016. URL:
  2. Jérôme Leroux, Grégoire Sutre, and Patrick Totzke. On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension. In ICALP, Part II, volume 9135 of LNCS, pages 324-336. Springer, 2015. URL:
  3. Charles Rackoff. The Covering and Boundedness Problems for Vector Addition Systems. Theor. Comput. Sci., 6:223-231, 1978. URL:
  4. Louis E. Rosier and Hsu-Chun Yen. A Multiparameter Analysis of the Boundedness Problem for Vector Addition Systems. J. Comput. Syst. Sci., 32(1):105-135, 1986. URL:
  5. Juliusz Straszyński. Complexity of the reachability problem for pushdown Petri nets. Master’s thesis, University of Warsaw, Faculty of Mathematics, Informatics, and Mechanics, 2017. URL: