Document Open Access Logo

Scope-Bounded Reachability in Valence Systems

Authors Aneesh K. Shetty, S. Krishna , Georg Zetzsche

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2021.29.pdf
  • Filesize: 0.96 MB
  • 19 pages

Document Identifiers

Author Details

Aneesh K. Shetty
  • Department of Computer Science & Engineering IIT Bombay, India
S. Krishna
  • Department of Computer Science & Engineering IIT Bombay, India
Georg Zetzsche
  • Max Planck Institute for Software Systems, Kaiserslautern, Germany

Cite AsGet BibTex

Aneesh K. Shetty, S. Krishna, and Georg Zetzsche. Scope-Bounded Reachability in Valence Systems. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 29:1-29:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CONCUR.2021.29

Abstract

Multi-pushdown systems are a standard model for concurrent recursive programs, but they have an undecidable reachability problem. Therefore, there have been several proposals to underapproximate their sets of runs so that reachability in this underapproximation becomes decidable. One such underapproximation that covers a relatively high portion of runs is scope boundedness. In such a run, after each push to stack i, the corresponding pop operation must come within a bounded number of visits to stack i. In this work, we generalize this approach to a large class of infinite-state systems. For this, we consider the model of valence systems, which consist of a finite-state control and an infinite-state storage mechanism that is specified by a finite undirected graph. This framework captures pushdowns, vector addition systems, integer vector addition systems, and combinations thereof. For this framework, we propose a notion of scope boundedness that coincides with the classical notion when the storage mechanism happens to be a multi-pushdown. We show that with this notion, reachability can be decided in PSPACE for every storage mechanism in the framework. Moreover, we describe the full complexity landscape of this problem across all storage mechanisms, both in the case of (i) the scope bound being given as input and (ii) for fixed scope bounds. Finally, we provide an almost complete description of the complexity landscape if even a description of the storage mechanism is part of the input.

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
  • Theory of computation → Formal languages and automata theory
Keywords
  • multi-pushdown systems
  • underapproximations
  • valence systems
  • reachability

Metrics

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

References

  1. C. Aiswarya, Paul Gastin, and K. Narayan Kumar. Verifying communicating multi-pushdown systems via split-width. In Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings, volume 8837 of Lecture Notes in Computer Science, pages 1-17. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-11936-6_1.
  2. S. Akshay, Paul Gastin, Shankara Narayanan Krishna, and Sparsa Roychowdhury. Revisiting underapproximate reachability for multipushdown systems. In Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I, volume 12078 of Lecture Notes in Computer Science, pages 387-404. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45190-5_21.
  3. Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. Linear-time model-checking for multithreaded programs under scope-bounding. In Automated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012, Thiruvananthapuram, India, October 3-6, 2012. Proceedings, volume 7561 of Lecture Notes in Computer Science, pages 152-166. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33386-6_13.
  4. Devendra Bhave, Shankara Narayanan Krishna, Ramchandra Phawade, and Ashutosh Trivedi. On timed scope-bounded context-sensitive languages. In Developments in Language Theory - 23rd International Conference, DLT 2019, Warsaw, Poland, August 5-9, 2019, Proceedings, volume 11647 of Lecture Notes in Computer Science, pages 168-181. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24886-4_12.
  5. P. Buckheister and Georg Zetzsche. Semilinearity and context-freeness of languages accepted by valence automata. In Mathematical Foundations of Computer Science 2013 - 38th International Symposium, MFCS 2013, Klosterneuburg, Austria, August 26-30, 2013. Proceedings, volume 8087 of Lecture Notes in Computer Science, pages 231-242. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40313-2_22.
  6. Aiswarya Cyriac. Verification of communicating recursive programs via split-width. (Vérification de programmes récursifs et communicants via split-width). PhD thesis, École normale supérieure de Cachan, France, 2014. URL: https://tel.archives-ouvertes.fr/tel-01015561.
  7. Aiswarya Cyriac, Paul Gastin, and K. Narayan Kumar. MSO decidability of multi-pushdown systems via split-width. In CONCUR 2012 - Concurrency Theory - 23rd International Conference, CONCUR 2012, Newcastle upon Tyne, UK, September 4-7, 2012. Proceedings, volume 7454 of Lecture Notes in Computer Science, pages 547-561. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32940-1_38.
  8. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for petri nets is not elementary. In Proceedings of STOC 2019, pages 24-33. ACM, 2019. URL: https://doi.org/10.1145/3313276.3316369.
  9. Stéphane Demri and Régis Gascon. The effects of bounding syntactic resources on presburger LTL. In Proceedings of TIME 2007, pages 94-104. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/TIME.2007.63.
  10. Emanuele D'Osualdo, Roland Meyer, and Georg Zetzsche. First-order logic with reachability for infinite-state systems. In Proceedings of LICS 2016, pages 457-466. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934552.
  11. Matthias Englert, Ranko Lazic, and Patrick Totzke. Reachability in two-dimensional unary vector addition systems with states is nl-complete. In Proceedings of LICS 2016, pages 477-484. ACM, 2016. URL: https://doi.org/10.1145/2933575.2933577.
  12. 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. URL: https://doi.org/10.1145/2629644.
  13. Eitan M. Gurari and Oscar H. Ibarra. The complexity of decision problems for finite-turn multicounter machines. Journal of Computer and System Sciences, 22(2):220-229, 1981. URL: https://doi.org/10.1016/0022-0000(81)90028-3.
  14. Christoph Haase and Simon Halfon. Integer vector addition systems with states. In Proceedings of RP 2014, volume 8762 of Lecture Notes in Computer Science, pages 112-124. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-11439-2_9.
  15. Christoph Haase and Georg Zetzsche. Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests. In Proceedings of LICS 2019, pages 1-14. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785850.
  16. Serge Haddad and Denis Poitrenaud. Recursive Petri nets. Acta Informatica, 44(7):463-508, 2007. Google Scholar
  17. Jérôme Leroux, Grégoire Sutre, and Patrick Totzke. On the coverability problem for pushdown vector addition systems in one dimension. In Proceedings of ICALP 2015, volume 9135 of Lecture Notes in Computer Science, pages 324-336. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_26.
  18. P. Madhusudan and Gennaro Parlato. The tree width of auxiliary storage. In Proceedings of POPL 2011, pages 283-294. ACM, 2011. URL: https://doi.org/10.1145/1926385.1926419.
  19. Roland Meyer, Sebastian Muskalla, and Georg Zetzsche. Bounded context switching for valence systems. In 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, volume 118 of LIPIcs, pages 12:1-12:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.12.
  20. Shaz Qadeer and Jakob Rehof. Context-bounded model checking of concurrent software. In Proceedings of TACAS 2005, pages 93-107. Springer, 2005. Google Scholar
  21. Ganesan Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. ACM Transactions on Programming languages and Systems (TOPLAS), 22(2):416-430, 2000. Google Scholar
  22. Salvatore La Torre and Margherita Napoli. Reachability of multistack pushdown systems with scope-bounded matching relations. In CONCUR 2011 - Concurrency Theory - 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings, volume 6901 of Lecture Notes in Computer Science, pages 203-218. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23217-6_14.
  23. Salvatore La Torre and Margherita Napoli. A temporal logic for multi-threaded programs. In Theoretical Computer Science - 7th IFIP TC 1/WG 2.2 International Conference, TCS 2012, Amsterdam, The Netherlands, September 26-28, 2012. Proceedings, volume 7604 of Lecture Notes in Computer Science, pages 225-239. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33475-7_16.
  24. Salvatore La Torre, Margherita Napoli, and Gennaro Parlato. Scope-bounded pushdown languages. Int. J. Found. Comput. Sci., 27(2):215-234, 2016. URL: https://doi.org/10.1142/S0129054116400074.
  25. Salvatore La Torre, Margherita Napoli, and Gennaro Parlato. Reachability of scope-bounded multistack pushdown systems. Inf. Comput., 275:104588, 2020. URL: https://doi.org/10.1016/j.ic.2020.104588.
  26. Salvatore La Torre and Gennaro Parlato. Scope-bounded multistack pushdown systems: Fixed-point, sequentialization, and tree-width. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012, December 15-17, 2012, Hyderabad, India, volume 18 of LIPIcs, pages 173-184. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2012.173.
  27. Georg Zetzsche. Silent transitions in automata with storage. In Proceedings of ICALP 2013, volume 7966 of Lecture Notes in Computer Science, pages 434-445. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_39.
  28. Georg Zetzsche. Computing downward closures for stacked counter automata. In Proceedings of STACS 2015, volume 30 of LIPIcs, pages 743-756. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.STACS.2015.743.
  29. Georg Zetzsche. Monoids as Storage Mechanisms. PhD thesis, Kaiserslautern University of Technology, Germany, 2016. URL: https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4400.
  30. Georg Zetzsche. Monoids as storage mechanisms. Bull. EATCS, 120, 2016. URL: http://eatcs.org/beatcs/index.php/beatcs/article/view/459.
  31. Georg Zetzsche. The emptiness problem for valence automata over graph monoids. Inf. Comput., 277:104583, 2021. URL: https://doi.org/10.1016/j.ic.2020.104583.
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