Document Open Access Logo

Unboundedness Problems for Languages of Vector Addition Systems

Authors Wojciech Czerwinski , Piotr Hofman , Georg Zetzsche

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2018.119.pdf
  • Filesize: 0.5 MB
  • 15 pages

Document Identifiers

Author Details

Wojciech Czerwinski
  • University of Warsaw, Poland
Piotr Hofman
  • University of Warsaw, Poland
Georg Zetzsche
  • IRIF (Université Paris-Diderot & CNRS), France

Funding

  • Czerwinski, Wojciech: Partially supported by the Polish National Science Centre grant 2016/21/D/ST6/01376
  • Hofman, Piotr: Partially supported by the Polish National Science Centre grant 2016/21/B/ST6/01505
  • Zetzsche, Georg: Supported by a fellowship of the Fondation Sciences Mathématiques de Paris and partially funded by the DeLTA project (ANR-16-CE40-0007). Part of the research was conducted when the author was supported by a fellowship within the Postdoc-Program of the German Academic Exchange Service (DAAD) and by Labex DigiCosme, Univ. Paris-Saclay, project VERICONISS.

Cite AsGet BibTex

Wojciech Czerwinski, Piotr Hofman, and Georg Zetzsche. Unboundedness Problems for Languages of Vector Addition Systems. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 119:1-119:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.ICALP.2018.119

Abstract

A vector addition system (VAS) with an initial and a final marking and transition labels induces a language. In part because the reachability problem in VAS remains far from being well-understood, it is difficult to devise decision procedures for such languages. This is especially true for checking properties that state the existence of infinitely many words of a particular shape. Informally, we call these unboundedness properties. We present a simple set of axioms for predicates that can express unboundedness properties. Our main result is that such a predicate is decidable for VAS languages as soon as it is decidable for regular languages. Among other results, this allows us to show decidability of (i) separability by bounded regular languages, (ii) unboundedness of occurring factors from a language K with mild conditions on K, and (iii) universality of the set of factors.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Formal languages and automata theory
Keywords
  • vector addition systems
  • decision problems
  • unboundedness
  • separability

Metrics

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

References

  1. Mohamed Faouzi Atig and Pierre Ganty. Approximating Petri net reachability along context-free traces. In FSTTCS 2011, volume 13, pages 152-163, Dagstuhl, Germany, 2011. Google Scholar
  2. Mohamed Faouzi Atig and Peter Habermehl. On Yen’s path logic for Petri nets. Int. J. Found. Comput. Sci., 22(4):783-799, 2011. Google Scholar
  3. Jean Berstel. Transductions and Context-Free Languages. Teubner, 1979. Google Scholar
  4. Michel Blockelet and Sylvain Schmitz. Model checking coverability graphs of vector addition systems. In MFCS 2011, pages 108-119, Berlin, Heidelberg, 2011. Springer. Google Scholar
  5. Mikołaj Bojańczyk. It is undecidable if two regular tree languages can be separated by a deterministic tree-walking automaton. Fundam. Inform., 154(1-4):37-46, 2017. Google Scholar
  6. Rémi Bonnet, Alain Finkel, Jérôme Leroux, and Marc Zeitoun. Place-Boundedness for Vector Addition Systems with one zero-test. In FSTTCS 2010, pages 192-203, 2010. Google Scholar
  7. Ahmed Bouajjani, Javier Esparza, and Tayssir Touili. A generic approach to the static analysis of concurrent programs with procedures. International Journal of Foundations of Computer Science, 14(04):551-582, 2003. Google Scholar
  8. Sagar Chaki, Edmund M. Clarke, Nicholas A. Kidd, Thomas W. Reps, and Tayssir Touili. Verifying Concurrent Message-Passing C Programs with Recursive Calls, pages 334-349. Springer-Verlag, Berlin Heidelberg, 2006. URL: http://dx.doi.org/10.1007/11691372_22.
  9. Pierre Chambart, Alain Finkel, and Sylvain Schmitz. Forward analysis and model checking for trace bounded WSTS. Theoretical Computer Science, 637:1-29, 2016. Google Scholar
  10. Lorenzo Clemente, Wojciech Czerwiński, Sławomir Lasota, and Charles Paperman. Regular separability of Parikh automata. In ICALP 2017, July 10-14, 2017, Warsaw, Poland, pages 117:1-117:13, 2017. Google Scholar
  11. Lorenzo Clemente, Wojciech Czerwiński, Sławomir Lasota, and Charles Paperman. Separability of reachability sets of vector addition systems. In STACS 2017, March 8-11, 2017, Hannover, Germany, pages 24:1-24:14, 2017. Google Scholar
  12. Thomas Colcombet. Regular cost functions, part I: logic and algebra over words. Logical Methods in Computer Science, 9(3), 2013. Google Scholar
  13. Wojciech Czerwiński and Sławomir Lasota. Regular separability of one counter automata. In LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12, 2017. Google Scholar
  14. Wojciech Czerwiński, Sławomir Lasota, Roland Meyer, Sebastian Muskalla, K Narayan Kumar, and Prakash Saivasan. Regular separability of well structured transition systems. CoRR, abs/1702.05334, 2018. Google Scholar
  15. Wojciech Czerwiński, Wim Martens, Lorijn van Rooijen, Marc Zeitoun, and Georg Zetzsche. A characterization for decidable separability by piecewise testable languages. Discrete Mathematics & Theoretical Computer Science, 19(4), 2017. Google Scholar
  16. Stéphane Demri. On selective unboundedness of VASS. In Proceedings of the 12th International Workshops on Verification of Infinite State Systems (INFINITY'10), volume 39 of Electronic Proceedings in Theoretical Computer Science, pages 1-15, Singapore, 2010. URL: http://dx.doi.org/10.4204/EPTCS.39.1.
  17. Stéphane Demri, Alain Finkel, Valentin Goranko, and Govert van Drimmelen. Model-checking CTL* over flat Presburger counter systems. Journal of Applied Non-Classical Logics, 20(4):313-344, 2010. Google Scholar
  18. Javier Esparza and Pierre Ganty. Complexity of pattern-based verification for multithreaded programs. In POPL 2011, pages 499-510, 2011. Google Scholar
  19. Javier Esparza, Pierre Ganty, and Rupak Majumdar. A perfect model for bounded verification. In LICS 2012, pages 285-294, 2012. Google Scholar
  20. Javier Esparza, Pierre Ganty, and Tomás Poch. Pattern-based verification for multithreaded programs. ACM Trans. Program. Lang. Syst., 36(3):9:1-9:29, 2014. Google Scholar
  21. Pierre Ganty, Rupak Majumdar, and Benjamin Monmege. Bounded underapproximations. Formal Methods in System Design, 40(2):206-231, 2012. Google Scholar
  22. Paweł Gawrychowski, Dalia Krieger, Narad Rampersad, and Jeffrey Shallit. Finding the growth rate of a regular or context-free language in polynomial time. International Journal of Foundations of Computer Science, 21(04):597-618, 2010. Google Scholar
  23. Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. Well-structured languages. Acta Informatica, 44(3-4):249-288, 2007. Google Scholar
  24. Seymour Ginsburg and Edwin H Spanier. Bounded algol-like languages. Transactions of the American Mathematical Society, 113(2):333-368, 1964. Google Scholar
  25. Seymour Ginsburg and Edwin H. Spanier. Bounded regular sets. Proceedings of the American Mathematical Society, 17(5):1043-1049, 1966. URL: http://dx.doi.org/10.2307/2036087.
  26. Jean Goubault-Larrecq and Sylvain Schmitz. Deciding piecewise testable separability for regular tree languages. In ICALP 2016, July 11-15, 2016, Rome, Italy, pages 97:1-97:15, 2016. Google Scholar
  27. Sheila A. Greibach. Remarks on blind and partially blind one-way multicounter machines. Theoretical Computer Science, 7(3):311-324, 1978. URL: http://dx.doi.org/10.1016/0304-3975(78)90020-8.
  28. Peter Habermehl, Roland Meyer, and Harro Wimmel. The downward-closure of Petri net languages. In ICALP 2010, volume 6199 of Lecture Notes in Computer Science, pages 466-477. Springer-Verlag, 2010. Google Scholar
  29. Matthew Hague and Anthony Widjaja Lin. Model checking recursive programs with numeric data types. In CAV 2011, volume 6806 of Lecture Notes in Computer Science, pages 743-759. Springer-Verlag, 2011. Google Scholar
  30. Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre. Collapsible pushdown automata and recursion schemes. In LICS 2008, pages 452-461, 2008. Google Scholar
  31. Leonard H. Haines. On free monoids partially ordered by embedding. Journal of Combinatorial Theory, 6(1):94-98, 1969. URL: http://dx.doi.org/10.1016/S0021-9800(69)80111-0.
  32. Dirk Hauschildt. Semilinearity of the reachability set is decidable for Petri nets. PhD thesis, Fachbereich Informatik, Universität Hamburg, 1990. Also available as Technical Report No. FBI-HH-B-146/90, Fachbereich Informatik, University of Hamburg. Google Scholar
  33. Dirk Hauschildt and Matthias Jantzen. Petri net algorithms in the theory of matrix grammars. Acta Informatica, 31(8):719-728, Aug 1994. Google Scholar
  34. Graham Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society. Third Series, 2:326-336, 1952. URL: http://dx.doi.org/10.1112/plms/s3-2.1.326.
  35. John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Reading, Massachusetts, 1979. Google Scholar
  36. Matthias Jantzen. On the hierarchy of petri net languages. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, 13(1):19-30, 1979. URL: http://www.numdam.org/item?id=ITA_1979__13_1_19_0.
  37. S. Rao Kosaraju. Decidability of reachability in vector addition systems (preliminary version). In STOC 1982, May 5-7, 1982, San Francisco, California, USA, pages 267-281, 1982. Google Scholar
  38. Jean-Luc Lambert. A structure to decide reachability in Petri nets. Theor. Comput. Sci., 99(1):79-104, 1992. Google Scholar
  39. Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems demystified. In LICS 2015, 2015. Google Scholar
  40. Jérôme Leroux, Grégoire Sutre, and Patrick Totzke. On the coverability problem for pushdown vector addition systems in one dimension. In ICALP 2015, pages 324-336, Berlin Heidelberg, 2015. Springer-Verlag. URL: http://dx.doi.org/10.1007/978-3-662-47666-6_26.
  41. Zhenyue Long, Georgel Calin, Rupak Majumdar, and Roland Meyer. Language-theoretic abstraction refinement. In FASE 2012, pages 362-376. Springer, 2012. Google Scholar
  42. A. N. Maslov. Multilevel stack automata. Problems of Information Transmission, 12(1):38-42, 1976. Google Scholar
  43. Ernst W. Mayr. An algorithm for the general Petri net reachability problem. In STOC 1981, May 11-13, 1981, Milwaukee, Wisconsin, USA, pages 238-246, 1981. Google Scholar
  44. Thomas Place and Marc Zeitoun. Concatenation hierarchies: New bottle, old wine. In CSR 2017, Kazan, Russia, June 8-12, 2017, Proceedings, pages 25-37, 2017. Google Scholar
  45. Thomas Place and Marc Zeitoun. Separation for dot-depth two. In LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12, 2017. Google Scholar
  46. Klaus Reinhardt. The "trio-zoo" - classes of formal languages generated from one language by rational transduction. Unpublished manuscript. Google Scholar
  47. Klaus Reinhardt. Reachability in Petri nets with inhibitor arcs. Electronic Notes in Theoretical Computer Science, 223:239-264, 2008. Proceedings of the Second Workshop on Reachability Problems in Computational Models (RP 2008). URL: http://dx.doi.org/10.1016/j.entcs.2008.12.042.
  48. George S. Sacerdote and Richard L. Tenney. The decidability of the reachability problem for vector addition systems (preliminary version). In STOC 1977, pages 61-76. ACM, 1977. Google Scholar
  49. Rani Siromoney. A characterization of semilinear sets. Proceedings of the American Mathematical Society, 21(3):689-694, 1969. Google Scholar
  50. Hsu-Chun Yen. A unified approach for deciding the existence of certain Petri net paths. Information and Computation, 96(1):119-137, 1992. Google Scholar
  51. Georg Zetzsche. The emptiness problem for valence automata over graph monoids. To appear in Information and Computation. Google Scholar
  52. Georg Zetzsche. An approach to computing downward closures. In ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, pages 440-451, 2015. 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