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

lmcs:921 - Logical Methods in Computer Science, September 27, 2012, Volume 8, Issue 3
Reachability Analysis of Communicating Pushdown Systems

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

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.


Source : oai:arXiv.org:1209.0359
DOI : 10.2168/LMCS-8(3:23)2012
Volume: Volume 8, Issue 3
Published on: September 27, 2012
Submitted on: December 15, 2010
Keywords: Computer Science - Logic in Computer Science,Computer Science - Formal Languages and Automata Theory,D.2.4, F.2


Share

Consultation statistics

This page has been seen 70 times.
This article's PDF has been downloaded 13 times.