Reachability Analysis of Communicating Pushdown Systems
Alexander Heussner (LaBRI, Universit\'e de Bordeaux, CNRS, France),, J\'er\^ome Leroux (LaBRI, Universit\'e de Bordeaux, CNRS, France), Anca, Muscholl (LaBRI, Universit\'e de Bordeaux, CNRS, France), Gr\'egoire Sutre, (LaBRI, Universit\'e de Bordeaux, CNRS, France)
TL;DR
This paper investigates the decidability and complexity of reachability analysis in communicating pushdown systems, providing new characterizations and algorithms for eager runs and bounded contexts, extending prior research.
Contribution
It introduces a characterization of communication topologies with decidable reachability for eager runs and develops a doubly exponential time algorithm for bounded context analysis.
Findings
Decidable reachability for eager runs is EXPTIME-complete.
A doubly exponential time algorithm is provided for bounded context analysis.
The results extend and improve previous work by La Torre et al.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.