6 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…
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…
Reachability in VASS Extended with Integer Counters
Clotilde Bizière, Wojciech Czerwiński, Roland Guttenberg +5
We consider a variant of VASS extended with integer counters, denoted VASS+Z. These are automata equipped with N and Z counters; the N-counters are required to remain nonnegative a…
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 One-Dimensional Pushdown Vector Addition Systems is Decidable
Clotilde Bizière, Wojciech Czerwiński
We consider the model of one-dimensional Pushdown Vector Addition Systems (1-PVAS), a fundamental computational model simulating both recursive and concurrent behaviours. Our main…