Reachability Analysis of Communicating Pushdown Systems

Alexander Heussner; Jérôme Leroux; Anca Muscholl; Grégoire Sutre

doi:10.2168/LMCS-8(3:23)2012

Alexander Heussner ; Jérôme Leroux ; Anca Muscholl ; Grégoire Sutre - Reachability Analysis of Communicating Pushdown Systems

lmcs:921 - Logical Methods in Computer Science, September 27, 2012, Volume 8, Issue 3 - https://doi.org/10.2168/LMCS-8(3:23)2012

Reachability Analysis of Communicating Pushdown SystemsArticle

Authors: Alexander Heussner ; Jérôme Leroux ; Anca Muscholl ; Grégoire Sutre

The reachability analysis of recursive programs that communicate asynchronously over reliable FIFO channels calls for restrictions to ensure decidability. Our first result characterizes communication topologies with a decidable reachability problem restricted to eager runs (i.e., runs where messages are either received immediately after being sent, or never received).
The problem is EXPTIME-complete in the decidable case. The second result is a doubly exponential time algorithm for bounded context analysis in this setting, together with a matching lower bound. Both results extend and improve previous work from La Torre et al.

https://doi.org/10.2168/LMCS-8(3:23)2012

Source: arXiv.org:1209.0359

Volume: Volume 8, Issue 3

Secondary volumes: Selected Papers of the 13th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2010)

Published on: September 27, 2012

Imported on: December 15, 2010

Keywords: Computer Science - Logic in Computer Science, Computer Science - Formal Languages and Automata Theory, D.2.4, F.2

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

16 Documents citing this article

Chris Köcher;Dietrich Kuske, 2023, Forwards- and Backwards-Reachability for Cooperating Multi-pushdown Systems, Lecture notes in computer science, pp. 318-332, 10.1007/978-3-031-43587-4_23.

Cinzia Di Giusto;Loïc Germerie Guizouarn;Etienne Lozes, 2022, Multiparty half-duplex systems and synchronous communications, Journal of Logical and Algebraic Methods in Programming, 131, pp. 100843, 10.1016/j.jlamp.2022.100843.

Felix Stutz;Damien Zufferey, 2022, Comparing Channel Restrictions of Communicating State Machines, High-level Message Sequence Charts, and Multiparty Session Types, Electronic Proceedings in Theoretical Computer Science, 370, pp. 194-212, 10.4204/eptcs.370.13, https://doi.org/10.4204/eptcs.370.13.

Lorenzo Clemente;Sławomir Lasota, 2020, Reachability relations of timed pushdown automata, arXiv (Cornell University), 117, pp. 202-241, 10.1016/j.jcss.2020.11.003, http://arxiv.org/abs/2012.15291.

Ahmed Bouajjani;Constantin Enea;Kailiang Ji;Shaz Qadeer, 2018, On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony, Lecture notes in computer science, pp. 372-391, 10.1007/978-3-319-96142-2_23, https://doi.org/10.1007/978-3-319-96142-2_23.

Meyer, Roland;Muskalla, Sebastian;Zetzsche, Georg, 2018, Bounded Context Switching for Valence Systems, arXiv (Cornell University), 10.4230/lipics.concur.2018.12, http://arxiv.org/abs/1803.09703.

Constantin Enea;Peter Habermehl;Omar Inverso;Gennaro Parlato, 2016, On the path-width of integer linear programming, Information and Computation, 253, pp. 257-271, 10.1016/j.ic.2016.07.010.

Dario Carotenuto;Aniello Murano;Adriano Peron, 2016, Ordered multi-stack visibly pushdown automata, Theoretical Computer Science, 656, pp. 1-26, 10.1016/j.tcs.2016.08.012.

Rayna Dimitrova;Rupak Majumdar, 2016, Reachability analysis of reversal-bounded automata on series–parallel graphs, Acta Informatica, 55, 2, pp. 153-189, 10.1007/s00236-016-0290-1, https://doi.org/10.1007/s00236-016-0290-1.

Gilles Geeraerts;Alexander Heußner;Jean-François Raskin, 2015, On the Verification of Concurrent, Asynchronous Programs with Waiting Queues, ACM Transactions on Embedded Computing Systems, 14, 3, pp. 1-26, 10.1145/2700072.

Benedikt Bollig;Paul Gastin;Jana Schubert, 2014, Parameterized Verification of Communicating Automata under Context Bounds, Lecture notes in computer science, pp. 45-57, 10.1007/978-3-319-11439-2_4.

C. Aiswarya;Paul Gastin;K. Narayan Kumar, 2014, Controllers for the Verification of Communicating Multi-pushdown Systems, Lecture notes in computer science, pp. 297-311, 10.1007/978-3-662-44584-6_21.

Constantin Enea;Peter Habermehl;Omar Inverso;Gennaro Parlato, 2014, On the Path-Width of Integer Linear Programming, Electronic Proceedings in Theoretical Computer Science, 161, pp. 74-87, 10.4204/eptcs.161.9, https://doi.org/10.4204/eptcs.161.9.

Lorenzo Clemente;Frédéric Herbreteau;Grégoire Sutre, 2014, Decidable Topologies for Communicating Automata with FIFO and Bag Channels, pp. 281-296, 10.1007/978-3-662-44584-6_20, https://hal.science/hal-01023456.

Parosh Aziz Abdulla;Mohamed Faouzi Atig;Jari Stenman, 2014, Zenoness for Timed Pushdown Automata, Electronic Proceedings in Theoretical Computer Science, 140, pp. 35-47, 10.4204/eptcs.140.3, https://doi.org/10.4204/eptcs.140.3.

Parosh Aziz Abdulla;Mohamed Faouzi Atig;Jonathan Cederberg, 2013, Analysis of Message Passing Programs Using SMT-Solvers, Lecture notes in computer science, pp. 272-286, 10.1007/978-3-319-02444-8_20.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3310 times.

This article's PDF has been downloaded 506 times.