AI summaryⓘ
The authors figured out how to determine if a certain state (configuration) can be reached in a complex system called a branching vector addition system (BVAS), which was a problem experts hadn't solved before. They showed that if a state can't be reached, there is a special kind of mathematical description (an inductive invariant made of semilinear sets) that proves it. Using this insight, they created a straightforward algorithm that checks reachability by systematically exploring these sets. This work solves a longstanding challenge in understanding BVAS behavior.
Branching Vector Addition SystemsReachability ProblemInductive InvariantsSemilinear SetsAlgorithmConfigurationEnumerative AlgorithmState SpaceSystem Verification
Authors
Clotilde Bizière, Jérôme Leroux, Grégoire Sutre
Abstract
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 invariants. More precisely, we prove that if a configuration of a BVAS is not reachable, then there exists an inductive invariant, given as a semilinear set, that does not contain this configuration. Based on this property, we deduce a very simple (enumerative) algorithm solving the reachability problem for BVAS.