34 citations · 60 across the 12 of their papers we have counts for
13 papers
Bridging the Gap Between Plain VASS and Branching VASS
Clotilde Bizière, Jérôme Leroux, Grégoire Sutre
Vectors addition systems with states (VASS), a model equivalent to Petri nets, are finite-state machines with finitely many counters ranging over the natural numbers. The decidable…
Solving the Reachability Problem for Branching Vector Addition Systems via Semilinear Inductive Invariants
Clotilde Bizière, Jérôme Leroux, Grégoire Sutre
In this paper, we solve the reachability problem for branching vector addition systems (BVAS), a long standing open problem. Our approach is based on semilinear inductive invariant…
On Parameterized Verification Over Tree Topologies
Romain Delpy, Anca Muscholl, Grégoire Sutre
Parameterized verification of finite-state processes with rendez-vous synchronization is notoriously undecidable when processes are linearly ordered. In this paper we study two kin…
A Forward-Only Construction of Semilinear Inductive Invariants for VAS
Clotilde Bizière, Jérôme Leroux, Grégoire Sutre
The reachability problem for Vector Addition Systems (VAS) is a central decision problem in the theory of infinite-state systems, first solved by Kosaraju and Mayr in the 1980s. An…
On the Reachability Problem for Two-Dimensional Branching VASS
Clotilde Bizière, Thibault Hilaire, Jérôme Leroux +1
Vectors addition systems with states (VASS), or equivalently Petri nets, are arguably one of the most studied formalisms for the modeling and analysis of concurrent systems. A cent…
Reachability in Two-Dimensional Vector Addition Systems with States: One Test is for Free
Jérôme Leroux, Grégoire Sutre
Vector addition system with states is an ubiquitous model of computation with extensive applications in computer science. The reachability problem for vector addition systems is ce…
On Functions Weakly Computable by Pushdown Petri Nets and Related Systems
J. Leroux, M. Praveen, Ph. Schnoebelen +1
We consider numerical functions weakly computable by grammar-controlled vector addition systems (GVASes, a variant of pushdown Petri nets). GVASes can weakly compute all fast growi…
Occam's Razor Applied to the Petri Net Coverability Problem
Thomas Geffroy, Jérôme Leroux, Grégoire Sutre
The verification of safety properties for concurrent systems often reduces to the coverability problem for Petri nets. This problem was shown to be ExpSpace-complete forty years ag…
On Boundedness Problems for Pushdown Vector Addition Systems
Jérôme Leroux, Grégoire Sutre, Patrick Totzke
We study pushdown vector addition systems, which are synchronized products of pushdown automata with vector addition systems. The question of the boundedness of the reachability se…
On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension
Jérôme Leroux, Grégoire Sutre, Patrick Totzke
Does the trace language of a given vector addition system (VAS) intersect with a given context-free language? This question lies at the heart of several verification questions invo…
Reachability of Communicating Timed Processes
Lorenzo Clemente, Frédéric Herbreteau, Amélie Stainer +1
We study the reachability problem for communicating timed processes, both in discrete and dense time. Our model comprises automata with local timing constraints communicating over…
Reachability Analysis of Communicating Pushdown Systems
Alexander Heussner, Jérôme Leroux, Anca Muscholl +1
The reachability analysis of recursive programs that communicate asynchronously over reliable FIFO channels calls for restrictions to ensure decidability. Our first result characte…
Accelerated Data-Flow Analysis
Jérôme Leroux, Gregoire Sutre
Acceleration in symbolic verification consists in computing the exact effect of some control-flow loops in order to speed up the iterative fix-point computation of reachable states…