3 papers
cs.LO2026
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…
cs.LO2026
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…
cs.LO2025
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…