Heußner, Alexander; Leroux, Jérôme; Muscholl, Anca; Sutre, Grégoire Reachability analysis of communicating pushdown systems. (English) Zbl 1248.68330 Log. Methods Comput. Sci. 8, No. 3, Paper No. 23, 20 p. (2012). Summary: 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 [S. La Torre, P. Madhusudan and G. Parlato, Lect. Notes Comput. Sci. 4963, 299–314 (2008; Zbl 1134.68446)]. Cited in 12 Documents MSC: 68Q60 Specification and verification (program logics, model checking, etc.) 68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) 68Q25 Analysis of algorithms and problem complexity 68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) Keywords:reachability analysis; communicating processes; pushdown systems Citations:Zbl 1134.68446 PDFBibTeX XMLCite \textit{A. Heußner} et al., Log. Methods Comput. Sci. 8, No. 3, Paper No. 23, 20 p. (2012; Zbl 1248.68330) Full Text: DOI