REACHABILITY ANALYSIS OF COMMUNICATING PUSHDOWN SYSTEMS

The reachability analysis of recursive programs that communicate asynchro-nously over reliable Fifo channels calls for restrictions to ensure decidability. Our first result characterizes communication topologies with a decidable reachability problem re-stricted 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 [21]