Search

• < Previous
• 1
• Next >

---

Reachability Analysis of Communicating Pushdown Systems

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&nbsp;[&hellip;]

---

Model Checking Vector Addition Systems with one zero-test

Rémi Bonnet ; Alain FInkel ; Jérôme Leroux ; Marc Zeitoun.

We design a variation of the Karp-Miller algorithm to compute, in a forward manner, a finite representation of the cover (i.e., the downward closure of the reachability set) of a vector addition system with one zero-test. This algorithm yields decision procedures for several problems for these&nbsp;[&hellip;]

---