Expand, Enlarge, and Check for Branching Vector Addition Systems
Expand, enlarge, and check (EEC) is a successful heuristic for the coverability problem of well-structured transition systems. EEC constructs a sequence of under- and over-approximations with the property that the presence of a bug is eventually exhibited by some under-approximation and the absence of a bug is eventually exhibited by some over-approximation.
In this paper, we consider the application of EEC to the coverability problem for branching vector addition systems (BVAS), an expressive model that subsumes Petri nets. We describe an EEC algorithm for BVAS, and prove its termination and correctness. We prove an upper bound on the number of iterations for our EEC algorithm, both for BVAS and, as a special case, vector addition systems (or Petri nets). We show that in addition to practical effectiveness, the EEC heuristic is asymptotically optimal. For BVAS, it requires at most doubly-exponentially many iterations, thus matching the optimal 2EXPTIME upper bound. For Petri nets, it can be implemented in EXPSPACE, again matching the optimal bound.