2 papers
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…