Skip to Main content Skip to Navigation
Conference papers

A scalable algebraic method to infer quadratic invariants of switched systems

Abstract : We present a new numerical abstract domain based on ellip- soids designed for the formal verification of switched linear systems. Unlike the existing approaches, this domain does not rely on a user-given template. We overcome the diffi- culty that ellipsoids do not have a lattice structure by ex- hibiting a canonical operator over-approximating the union. This operator is the only one which permits to perform anal- yses that are invariant with respect to a linear transforma- tion of state variables. Moreover, we show that this operator can be computed efficiently using basic algebraic operations on positive semidefinite matrices. We finally develop a fast non-linear power-type algorithm, which allows one to de- termine sound quadratic invariants on switched systems in a tractable way, by solving fixed point problems over the space of ellipsoids. We test our approach on several bench- marks, and compare it with the standard techniques based on linear matrix inequalities, showing an important speedup on typical instances.
Complete list of metadata
Contributor : Stephane Gaubert <>
Submitted on : Thursday, December 31, 2015 - 3:06:17 PM
Last modification on : Tuesday, December 8, 2020 - 9:45:37 AM




Xavier Allamigeon, Stéphane Gaubert, Eric Goubault, Sylvie Putot, Nikolas Stott. A scalable algebraic method to infer quadratic invariants of switched systems. International Conference on Embedded Software (EMSOFT'2015), Alain Girault, INRIA, Grenoble, France and Nan Guan, Northeastern University, China, Oct 2015, Amsterdam, Netherlands. ⟨10.1109/EMSOFT.2015.7318262⟩. ⟨hal-01249320⟩



Record views