Semi-linear VASR for Over-Approximate Semi-linear Transition System Reachability

This paper introduces Semi-Linear Integer Vector Addition Systems with Resets (SVASR). A SVASR is a labeled transition system in which the states are finite-dimensional integer-valued vectors and which transitions from one state to another by applying an orthogonal projection followed by a translation drawn from a semi-linear set. We give a polynomial-time reduction of SVASR reachability to that of Integer Vector Addition Systems with Resets. We then consider the use of SVASRs for over-approximating the reachability relation of transition systems in which the transition relation is a semi-linear set. We show that any semi-linear transition system has a “best” SVASR that simulates its behavior, called its SVASR-reflection. The dimension of the SVASR-reflection of a semi-linear transition system T with states is exponential in the number of states; however, we show that the over-approximate reachability induced by T’s SVASR-reflection can be computed in polynomial time.