Safety verification for linear systems

An embedded software controller is safe if the composition of the controller and the plant does not reach any unsafe state starting from legal initial states (in an unbounded time horizon). Linear systems - specified using linear ordinary differential or difference equations - form an important class of models for such control systems. We present a new decidability result for safety verification of linear systems. Our decidability result assumes that the set of initial states and the set of unsafe states satisfy some conditions. When the set of initial and unsafe states do not satisfy these conditions, they can be overapproximated by sets that do satisfy the conditions. We thus get a counterexample guided abstraction refinement (CEGAR) procedure for the unconstrained safety verification of linear systems. Our new procedure performs abstraction-refinement on the initial and unsafe region, and not on the system itself. We present the new procedure and describe experimental results that demonstrate its effectiveness.