Reachability sets of branching VASS are close to plain VASS sets

Bridging the Gap Between Plain VASS and Branching VASS

Logic in Computer ScienceFormal Languages and Automata Theory

Summary

Vectors addition systems with states (VASS) are mathematical models used to study processes with counters that only increase. Branching VASS (BVASS) generalize this by allowing branching or splitting of processes. The authors show that the sets describing where these processes can reach in BVASS are very similar to those in VASS, with a precise relationship between them. They also find a way to simplify BVASS behaviors into ones with limited branching, helping better understand their structure. This leads to new results about the shape of BVASS reachability sets, including that in five dimensions, they can be described by simple mathematical patterns.

What this means in practice

  • For software verification teams: Check more complex systems that involve branching behaviors by mapping them back to simpler counter models to verify reachability properties.
  • For formal methods engineers: Use the bounded branching complexity results to optimize model checking tools for systems incorporating both linear and branching counter processes.

A theory result. No direct application yet.

Authors

Clotilde Bizière, Jérôme Leroux, Grégoire Sutre

Abstract

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 reachability problem for VASS has many applications in logic, automata, and verification. In this paper we study the reachability problem for BVASS, a branching generalization of VASS. We show that BVASS reachability sets are very similar to VASS reachability sets, namely that they are sections of VASS. Our proof relies on a new well-quasi-order (wqo) on BVASS runs that generalizes the well-known wqo on VASS runs. By leveraging an amalgamation property, we prove that every BVASS run can be transformed into an equivalent one of bounded branching complexity. This allows us to derive several results on the geometry of BVASS reachability sets. As an application we obtain that reachability sets of 5-dimensional BVAS are effectively semilinear, as is the case for 5-dimensional VAS.
View PDFOpen arXiv