3 results
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 […]
Published on June 19, 2012
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 […]
Published on September 27, 2012
leroux jerome.
The reachability problem for Vector Addition Systems (VASs) is a central problem of net theory. The general problem is known to be decidable by algorithms exclusively based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition. This decomposition is used in this paper to prove that […]
Published on September 9, 2010