Search

• < Previous
• 1
• Next >

---

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;]

---

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;]

---

Structurally Cyclic Petri Nets

Drewes Frank ; Leroux Jérôme.

A Petri net is structurally cyclic if every configuration is reachable from itself in one or more steps. We show that structural cyclicity is decidable in deterministic polynomial time. For this, we adapt the Kosaraju's approach for the general reachability problem for Petri nets.

---