Geometric programming relaxations for linear system reachability

One of the main obstacles in the safety analysis of continuous and hybrid systems has been the computation of the reachable set for continuous systems in high dimensions. We present a novel method that exploits the structure of linear dynamical systems, and the monotonicity of the exponential function in order to obtain safety certificates of continuous linear systems. By over-approximating the sets of initial and final states, the safety verification problem is expressed as a series of geometric programs, which can be further, transformed into linear programs. This provides the ability to verify the safety properties of high dimensional linear systems with realistic computation times. In addition, our optimization-based formulation computes time intervals over which the system is safe and unsafe.