Document Open Access Logo

On the Length of Strongly Monotone Descending Chains over ℕ^d

Authors Sylvain Schmitz , Lia Schütze

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2024.153.pdf
  • Filesize: 0.86 MB
  • 19 pages

Document Identifiers

Author Details

Sylvain Schmitz
  • Université Paris Cité, CNRS, IRIF, Paris, France
Lia Schütze
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany

Cite AsGet BibTex

Sylvain Schmitz and Lia Schütze. On the Length of Strongly Monotone Descending Chains over ℕ^d. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 153:1-153:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ICALP.2024.153

Abstract

A recent breakthrough by Künnemann, Mazowiecki, Schütze, Sinclair-Banks, and Węgrzycki (ICALP 2023) bounds the running time for the coverability problem in d-dimensional vector addition systems under unary encoding to n^{2^{O(d)}}, improving on Rackoff’s n^{2^{O(dlg d)}} upper bound (Theor. Comput. Sci. 1978), and provides conditional matching lower bounds. In this paper, we revisit Lazić and Schmitz' "ideal view" of the backward coverability algorithm (Inform. Comput. 2021) in the light of this breakthrough. We show that the controlled strongly monotone descending chains of downwards-closed sets over ℕ^d that arise from the dual backward coverability algorithm of Lazić and Schmitz on d-dimensional unary vector addition systems also enjoy this tight n^{2^{O(d)}} upper bound on their length, and that this also translates into the same bound on the running time of the backward coverability algorithm. Furthermore, our analysis takes place in a more general setting than that of Lazić and Schmitz, which allows to show the same results and improve on the 2EXPSPACE upper bound derived by Benedikt, Duff, Sharad, and Worrell (LICS 2017) for the coverability problem in invertible affine nets.

Subject Classification

ACM Subject Classification
  • Theory of computation → Parameterized complexity and exact algorithms
  • Theory of computation → Models of computation
Keywords
  • Vector addition system
  • coverability
  • well-quasi-order
  • order ideal
  • affine net

Metrics

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

Related Versions

References

  1. Parosh A. Abdulla, Karlis Čerāns, Bengt Jonsson, and Yih-Kuen Tsay. Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation, 160(1-2):109-127, 2000. URL: https://doi.org/10.1006/inco.1999.2843.
  2. 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: https://doi.org/10.1016/0304-3975(76)90067-0.
  3. André Arnold and Michel Latteux. Récursivité et cônes rationnels fermés par intersection. CALCOLO, 15(4):381-394, 1978. URL: https://doi.org/10.1007/BF02576519.
  4. A. R. Balasubramanian. Complexity of controlled bad sequences over finite sets of ℕ^d. In Proceedings of LICS 2020, pages 130-140. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394753.
  5. A. R. Balasubramanian. Complexity of coverability in depth-bounded processes. In Proceedings of CONCUR 2022, volume 243 of Leibniz International Proceedings in Informatics, pages 17:1-17:19. LZI, 2022. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.17.
  6. A. R. Balasubramanian, Timo Lang, and Revantha Ramanayake. Decidability and complexity in weakening and contraction hypersequent substructural logics. In Proceedings of LICS 2021, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470733.
  7. Michael Benedikt, Timothy Duff, Aditya Sharad, and James Worrell. Polynomial automata: Zeroness and applications. In Proceedings of LICS 2017, pages 1-12. IEEE, 2017. URL: https://doi.org/10.1109/LICS.2017.8005101.
  8. Michael Blondin, Alain Finkel, Christoph Haase, and Serge Haddad. Approaching the coverability problem continuously. In Proceedings of TACAS 2016, volume 9636 of Lecture Notes in Computer Science, pages 480-496. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49674-9_28.
  9. Michael Blondin, Alain Finkel, and Pierre McKenzie. Handling infinitely branching well-structured transition systems. Information and Computation, 258:28-49, 2018. URL: https://doi.org/10.1016/j.ic.2017.11.001.
  10. Michael Blondin, Christoph Haase, and Philip Offtermatt. Directed reachability for infinite-state systems. In Proceedings of TACAS 2021, volume 12652 of Lecture Notes in Computer Science, pages 3-23. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_1.
  11. Rémi Bonnet, Alain Finkel, and M. Praveen. Extending the Rackoff technique to affine nets. In Proceedings of FSTTCS 2012, volume 18 of Leibniz International Proceedings in Informatics, pages 301-312. LZI, 2012. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2012.301.
  12. Robert Bonnet. On the cardinality of the set of initial intervals of a partially ordered set. In Infinite and finite sets: to Paul Erdős on his 60th birthday, Vol. 1, volume 10 of Coll. Math. Soc. János Bolyai, pages 189-198. North-Holland, 1975. Google Scholar
  13. Laura Bozzelli and Pierre Ganty. Complexity analysis of the backward coverability algorithm for VASS. In Proceedings of RP 2011, volume 6945 of Lecture Notes in Computer Science, pages 96-109. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-24288-5_10.
  14. Gianfranco Ciardo. Petri nets with marking-dependent arc cardinality: Properties and analysis. In Proceedings of Petri Nets 1994, volume 815 of Lecture Notes in Computer Science, pages 179-198. Springer, 1994. URL: https://doi.org/10.1007/3-540-58152-9_11.
  15. Jean-Baptiste Courtois and Sylvain Schmitz. Alternating vector addition systems with states. In Proceedings of MFCS 2014, volume 8634 of Lecture Notes in Computer Science, pages 220-231. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44522-8_19.
  16. Stéphane Demri, Marcin Jurdziński, Oded Lachish, and Ranko Lazić. The covering and boundedness problems for branching vector addition systems. Journal of Computer and System Sciences, 79(1):23-38, 2013. URL: https://doi.org/10.1016/j.jcss.2012.04.002.
  17. Leonard Eugene Dickson. Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. American Journal of Mathematics, 35(4):413-422, 1913. URL: https://doi.org/10.2307/2370405.
  18. Catherine Dufourd, Alain Finkel, and Philippe Schnoebelen. Reset nets between decidability and undecidability. In Proceedings of ICALP 1998, volume 1443 of Lecture Notes in Computer Science, pages 103-115. Springer, 1998. URL: https://doi.org/10.1007/BFb0055044.
  19. Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp Meyer, and Filip Niksic. An SMT-based approach to coverability analysis. In Proceedings of CAV 2014, volume 8559 of Lecture Notes in Computer Science, pages 603-619. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_40.
  20. Diego Figueira, Santiago Figueira, Sylvain Schmitz, and Philippe Schnoebelen. Ackermannian and primitive-recursive bounds with Dickson’s Lemma. In Proceedings of LICS 2011, pages 269-278. IEEE, 2011. URL: https://doi.org/10.1109/LICS.2011.39.
  21. Alain Finkel. A generalization of the procedure of Karp and Miller to well structured transition systems. In Proceedings of ICALP 1987, volume 267 of Lecture Notes in Computer Science, pages 499-508. Springer, 1987. URL: https://doi.org/10.1007/3-540-18088-5_43.
  22. Alain Finkel, Pierre McKenzie, and Claudine Picaronny. A well-structured framework for analysing Petri net extensions. Information and Computation, 195(1):1-29, 2004. URL: https://doi.org/10.1016/j.ic.2004.01.005.
  23. Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1-2):63-92, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00102-X.
  24. Thomas Geffroy, Jérôme Leroux, and Grégoire Sutre. Occam’s Razor applied to the Petri net coverability problem. Theoretical Computer Science, 750:38-52, 2018. URL: https://doi.org/10.1016/j.tcs.2018.04.014.
  25. Jean Goubault-Larrecq, Simon Halfon, Prateek Karandikar, K. Narayan Kumar, and Philippe Schnoebelen. The ideal approach to computing closed subsets in well-quasi-orderings. In Well-Quasi-Orders in Computation, Logic, Language and Reasoning, volume 53 of Trends in Logic, pages 55-105. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-30229-0_3.
  26. Lucie Guillou, Corto Mascle, and Nicolas Waldburger. Parameterized broadcast networks with registers: from NP to the frontiers of decidability. In Proceedings of FoSSaCS 2024, volume 14575 of Lecture Notes in Computer Science, pages 250-270, 2024. URL: https://doi.org/10.1007/978-3-031-57231-9_12.
  27. Richard M. Karp and Raymond E. Miller. Parallel program schemata. Journal of Computer and System Sciences, 3(2):147-195, 1969. URL: https://doi.org/10.1016/S0022-0000(69)80011-5.
  28. Ulla Koppenhagen and Ernst W. Mayr. Optimal algorithms for the coverability, the subword, the containment, and the equivalence problems for commutative semigroups. Information and Computation, 158(2):98-124, 2000. URL: https://doi.org/10.1006/inco.1999.2812.
  29. Joseph B. Kruskal. The theory of well-quasi-ordering: A frequently discovered concept. Journal of Combinatorial Theory, Series A, 13(3):297-305, 1972. URL: https://doi.org/10.1016/0097-3165(72)90063-5.
  30. Marvin Künnemann, Filip Mazowiecki, Lia Schütze, Henry Sinclair-Banks, and Karol Węgrzycki. Coverability in VASS revisited: Improving Rackoff’s bound to obtain conditional optimality. In Proceedings of ICALP 2023, Leibniz International Proceedings in Informatics, pages 131:1-131:20. LZI, 2023. URL: https://doi.org/10.4230/LIPIcs.ICALP.2023.131.
  31. Ranko Lazić and Sylvain Schmitz. The complexity of coverability in ν-Petri nets. In Proceedings of LICS 2016, pages 467-476. ACM, 2016. URL: https://doi.org/10.1145/2933575.2933593.
  32. Ranko Lazić and Sylvain Schmitz. The ideal view on Rackoff’s coverability technique. Information and Computation, 277:104582, 2021. URL: https://doi.org/10.1016/j.ic.2020.104582.
  33. Jérôme Leroux. Vector addition system reversible reachability problem. Logical Methods in Computer Science, 9(1), 2013. URL: https://doi.org/10.2168/LMCS-9(1:5)2013.
  34. Richard J. Lipton. The reachability problem requires exponential space. Technical Report 62, Department of Computer Science, Yale University, 1976. URL: http://www.cs.yale.edu/publications/techreports/tr63.pdf.
  35. Ernst W. Mayr and Albert R. Meyer. The complexity of the word problems for commutative semigroups and polynomial ideals. Advances in Mathematics, 46(3):305-329, 1982. URL: https://doi.org/10.1016/0001-8708(82)90048-2.
  36. Dmitri Novikov and Sergei Yakovenko. Trajectories of polynomial vector fields and ascending chains of polynomial ideals. Annales de l’Institut Fourier, 49(2):563-609, 1999. URL: https://doi.org/10.5802/aif.1683.
  37. Charles Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6(2):223-231, 1978. URL: https://doi.org/10.1016/0304-3975(78)90036-1.
  38. Louis E. Rosier and Hsu-Chun Yen. A multiparameter analysis of the boundedness problem for vector addition systems. Journal of Computer and System Sciences, 32(1):105-135, 1986. URL: https://doi.org/10.1016/0022-0000(86)90006-1.
  39. Sylvain Schmitz. Algorithmic Complexity of Well-Quasi-Orders. Habilitation thesis, École Normale Supérieure Paris-Saclay, 2017. URL: http://tel.archives-ouvertes.fr/tel-01663266.
  40. Sylvain Schmitz. The parametric complexity of lossy counter machines. In Proceedings of ICALP 2019, volume 132 of Leibniz International Proceedings in Informatics, pages 129:1-129:15. LZI, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.129.
  41. Sylvain Schmitz and Philippe Schnoebelen. Algorithmic aspects of WQO theory. Lecture notes, 2012. URL: http://cel.archives-ouvertes.fr/cel-00727025.
  42. Philippe Schnoebelen. Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets. In Proceedings of MFCS 2010, volume 6281 of Lecture Notes in Computer Science, pages 616-628. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15155-2_54.
  43. Rüdiger Valk. Self-modifying nets, a natural extension of Petri nets. In Proceedings of ICALP 1978, volume 62 of Lecture Notes in Computer Science, pages 464-476. Springer, 1978. URL: https://doi.org/10.1007/3-540-08860-1_35.
  44. Hsu-Chun Yen and Chien-Liang Chen. On minimal elements of upward-closed sets. Theoretical Computer Science, 410(24):2442-2452, 2009. URL: https://doi.org/10.1016/j.tcs.2009.02.036.
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