Symbolic Reachability Computation for Families of Linear Vector Fields

Abstract

The control paradigm of physical processes being supervised by digital programs has lead to the development of a theory of hybrid systems combining finite state automata with differential equations. One of the most important problems in the verification of hybrid systems is the reachability problem. Even though the computation of reachable spaces for finite state machines is well developed, computing the reachable space of a differential equation is difficult. In this paper, we present the first known families of linear differential equations with a decidable reachability problem. This is achieved by posing the reachability computation as a quantifier elimination problem in the decidable theory of the reals. We illustrate the applicability of our approach by performing computations using the packages $\text{Redlog}$ and $\text{Qepcad}$. Such symbolic computations can be incorporated in computer-aided verification tools for purely discrete systems, resulting in verification tools for hybrid systems with linear differential equations.