Document Open Access Logo

Ideal Decompositions for Vector Addition Systems (Invited Talk)

Authors Jérôme Leroux, Sylvain Schmitz

PDF
Thumbnail PDF

File

LIPIcs.STACS.2016.1.pdf
  • Filesize: 0.66 MB
  • 13 pages

Document Identifiers

Author Details

Jérôme Leroux
Sylvain Schmitz

Cite AsGet BibTex

Jérôme Leroux and Sylvain Schmitz. Ideal Decompositions for Vector Addition Systems (Invited Talk). In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 1:1-1:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.STACS.2016.1

Abstract

Vector addition systems, or equivalently Petri nets, are one of the most popular formal models for the representation and the analysis of parallel processes. Many problems for vector addition systems are known to be decidable thanks to the theory of well-structured transition systems. Indeed, vector addition systems with configurations equipped with the classical point-wise ordering are well-structured transition systems. Based on this observation, problems like coverability or termination can be proven decidable. However, the theory of well-structured transition systems does not explain the decidability of the reachability problem. In this presentation, we show that runs of vector addition systems can also be equipped with a well quasi-order. This observation provides a unified understanding of the data structures involved in solving many problems for vector addition systems, including the central reachability problem.
Keywords
  • Petri net
  • ideal
  • well-quasi-order
  • reachability
  • verification

Metrics

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

References

  1. P. A. Abdulla, K. Čerāns, B. Jonsson, and Yih-Kuen Tsay. Algorithmic analysis of programs with well quasi-ordered domains. Inform. and Comput., 160(1-2):109-127, 2000. Google Scholar
  2. Parosh Aziz Abdulla, Aurore Collomb-Annichini, Ahmed Bouajjani, and Bengt Jonsson. Using forward reachability analysis for verification of lossy channel systems. Form. Methods in Syst. Des., 25(1):39-65, 2004. URL: http://dx.doi.org/10.1023/B:FORM.0000033962.51898.1a.
  3. Michel Blockelet and Sylvain Schmitz. Model-checking coverability graphs of vector addition systems. In MFCS 2011, volume 6907 of LNCS, pages 108-119. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-22993-0_13.
  4. Mikołaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data words. ACM Trans. Comput. Logic, 12(4):1-26, 2011. URL: http://dx.doi.org/10.1145/1970398.1970403.
  5. 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, Coll. Math. Soc. János Bolyai, pages 189-198. North-Holland, 1975. Google Scholar
  6. Laura Bozzelli and Pierre Ganty. Complexity analysis of the backward coverability algorithm for VASS. In Giorgio Delzanno and Igor Potapov, editors, Proc. RP 2011, volume 6945 of LNCS, pages 96-109. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-24288-5_10.
  7. E. Cardoza, Richard J. Lipton, and Albert R. Meyer. Exponential space complete problems for Petri nets and commutative semigroups: Preliminary report. In Proc. STOC'76, pages 50-54. ACM, 1976. URL: http://dx.doi.org/10.1145/800113.803630.
  8. Thomas Colcombet and Amaldev Manuel. Generalized data automata and fixpoint logic. In Proc. FSTTCS 2014, volume 29 of LIPIcs, pages 267-278. LZI, 2014. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.267.
  9. Jean-Baptiste Courtois and Sylvain Schmitz. Alternating vector addition systems with states. In Erzsébet Csuhaj-Varjú, Martin Dietzfelbinger, and Zoltán Ésik, editors, Proc. MFCS 2014, volume 8634 of LNCS, pages 220-231. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-662-44522-8_19.
  10. Wojciech Czerwiński, Wim Martens, Lorijn van Rooijen, Marc Zeitoun, and Georg Zetzsche. A characterization for decidable separability by piecewise testable languages. Preprint, 2015. Extended abstract published in Proc. FCT 2015. URL: http://arxiv.org/abs/1410.1042.
  11. Stéphane Demri. On selective unboundedness of VASS. Journal of Computer and System Sciences, 79(5):689-713, 2013. URL: http://dx.doi.org/10.1016/j.jcss.2013.01.014.
  12. Stéphane Demri, Diego Figueira, and M. Praveen. Reasoning about data repetitions with counter systems. In Proc. LICS 2013, pages 33-42. IEEE Press, 2013. URL: http://dx.doi.org/10.1109/LICS.2013.8.
  13. 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. Google Scholar
  14. Leonard Eugene Dickson. Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Amer. J. of Math., 35(4):413-422, 1913. URL: http://dx.doi.org/10.2307/2370405.
  15. Catherine Dufourd, Philippe Schnoebelen, and Petr Jančar. Boundedness of reset P/T nets. In Proc. ICALP'99, volume 1644 of LNCS, pages 301-310, 1999. URL: http://dx.doi.org/10.1007/3-540-48523-6_27.
  16. Diego Figueira, Santiago Figueira, Sylvain Schmitz, and Philippe Schnoebelen. Ackermannian and primitive-recursive bounds with Dickson’s Lemma. In Proc. LICS 2011, pages 269-278. IEEE Press, 2011. URL: http://dx.doi.org/10.1109/LICS.2011.39.
  17. Alain Finkel and Jean Goubault-Larrecq. Forward analysis for WSTS, part I: Completions. In Proc. STACS 2009, volume 3 of LIPIcs, pages 433-444. LZI, 2009. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2009.1844.
  18. Alain Finkel and Jean Goubault-Larrecq. Forward analysis for WSTS, part II: Complete WSTS. Logic. Meth. in Comput. Sci., 8(3:28):1-35, 2012. URL: http://dx.doi.org/10.2168/LMCS-8(3:28)2012.
  19. Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theor. Comput. Sci., 256(1-2):63-92, 2001. URL: http://dx.doi.org/10.1016/S0304-3975(00)00102-X.
  20. Pierre Ganty and Rupak Majumdar. Algorithmic verification of asynchronous programs. ACM Trans. Prog. Lang. Sys., 34(1):1-48, 2012. URL: http://dx.doi.org/10.1145/2160910.2160915.
  21. Jean Goubault-Larrecq, Prateek Karandikar, K. Narayan Kumar, and Philippe Schnoebelen. The ideal approach to computing closed subsets in well-quasi-orderings. In preparation, 2016. Google Scholar
  22. Peter Habermehl, Roland Meyer, and Harro Wimmel. The downward-closure of Petri net languages. In Proc. ICALP 2010, volume 6199 of LNCS, pages 466-477. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-14162-1_39.
  23. Graham Higman. Ordering by divisibility in abstract algebras. Proc. London Math. Soc., 3(2):326-336, 1952. URL: http://dx.doi.org/10.1112/plms/s3-2.1.326.
  24. Piotr Hofman, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, Sylvain Schmitz, and Patrick Totzke. Coverability trees for Petri nets with unordered data. In Proc. FoSSaCS 2016, LNCS. Springer, 2016. To appear. Google Scholar
  25. Paulin Jacobé de Naurois. Coverability in a non functional extension of BVASS. Preprint, 2014. Presented at CiE 2013. URL: https://hal.archives-ouvertes.fr/hal-00947136.
  26. Pierre Jullien. Contribution à l'étude des types d'ordres dispersés. Thèse de doctorat, Université de Marseille, 1969. Google Scholar
  27. M. Kabil and M. Pouzet. Une extension d'un théorème de P. Jullien sur les âges de mots. Theor. Inform. Appl., 26(5):449-482, 1992. Google Scholar
  28. 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.
  29. S. Rao Kosaraju. Decidability of reachability in vector addition systems. In Proc. STOC'82, pages 267-281. ACM, 1982. URL: http://dx.doi.org/10.1145/800070.802201.
  30. 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.
  31. Ranko Lazić. The reachability problem for vector addition systems with a stack is not elementary. Preprint, 2013. Presented at RP 2012. URL: http://arxiv.org/abs/1310.1767.
  32. Ranko Lazić, Tom Newcomb, Joël Ouaknine, A.W. Roscoe, and James Worrell. Nets with tokens which carry data. Fund. Inform., 88(3):251-274, 2008. Google Scholar
  33. Ranko Lazić and Sylvain Schmitz. The ideal view on Rackoff’s coverability technique. In Proc. RP 2015, volume 9328 of LNCS, pages 1-13. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-24537-9_8.
  34. Ranko Lazić and Sylvain Schmitz. Non-elementary complexities for branching VASS, MELL, and extensions. ACM Trans. Comput. Logic, 16(3), 2015. URL: http://dx.doi.org/10.1145/2733375.
  35. Jérôme Leroux. Presburger vector addition systems. In Proc. LICS 2013, pages 23-32. IEEE Press, 2013. URL: http://dx.doi.org/10.1109/LICS.2013.7.
  36. Jérôme Leroux, M. Praveen, and Grégoire Sutre. Hyper-Ackermannian bounds for pushdown vector addition systems. In Proc. CSL-LICS 2014. ACM, 2014. URL: http://dx.doi.org/10.1145/2603088.2603146.
  37. Jérôme Leroux and Sylvain Schmitz. Demystifying reachability in vector addition systems. In Proc. LICS 2015, pages 56-67. IEEE Press, 2015. URL: http://dx.doi.org/10.1109/LICS.2015.16.
  38. Jérôme Leroux, Grégoire Sutre, and Patrick Totzke. On the coverability problem for pushdown vector addition systems in one dimension. In Proc. ICALP 2015, volume 9135 of LNCS, pages 324-336. Springer, 2015. Google Scholar
  39. M.H. Löb and S.S. Wainer. Hierarchies of number-theoretic functions. I. Arch. Math. Logic, 13(1-2):39-51, 1970. URL: http://dx.doi.org/10.1007/BF01967649.
  40. Ernst W. Mayr. An algorithm for the general Petri net reachability problem. In Proc. STOC'81, pages 238-246. ACM, 1981. URL: http://dx.doi.org/10.1145/800076.802477.
  41. E.W. Mayr and A.R. Meyer. The complexity of the finite containment problem for Petri nets. Journal of the ACM, 28(3):561-576, 1981. URL: http://dx.doi.org/10.1145/322261.322271.
  42. Kenneth McAloon. Petri nets and large finite sets. Theor. Comput. Sci., 32(1-2):173-183, 1984. Google Scholar
  43. Horst Müller. The reachability problem for VAS. In Advances in Petri Nets 1984, volume 188 of LNCS, pages 376-391. Springer, 1985. URL: http://dx.doi.org/10.1007/3-540-15204-0_21.
  44. Charles Rackoff. The covering and boundedness problems for vector addition systems. Theor. Comput. Sci., 6(2):223-231, 1978. URL: http://dx.doi.org/10.1016/0304-3975(78)90036-1.
  45. Christophe Reutenauer. The mathematics of Petri nets. Masson and Prentice, 1990. Google Scholar
  46. George S. Sacerdote and Richard L. Tenney. The decidability of the reachability problem for vector addition systems. In Proc. STOC'77, pages 61-76. ACM, 1977. URL: http://dx.doi.org/10.1145/800105.803396.
  47. Sylvain Schmitz. On the computational complexity of dominance links in grammatical formalisms. In Proc. ACL 2010, pages 514-524. ACL Press, 2010. Google Scholar
  48. Sylvain Schmitz. Automata column: The complexity of reachability in vector addition systems. ACM SigLog News, 3(1), 2016. To appear. Google Scholar
  49. Kumar Neeraj Verma and Jean Goubault-Larrecq. Karp-Miller trees for a branching extension of VASS. Disc. Math. and Theor. Comput. Sci., 7(1):217-230, 2005. URL: http://www.dmtcs.org/volumes/abstracts/dm070113.abs.html.
  50. Georg Zetzsche. An approach to computing downward closures. In Proc. ICALP 2015, volume 9135 of LNCS, pages 440-451. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-47666-6_35.
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