Skip to Main content Skip to Navigation
Journal articles

A scalable algebraic method to infer quadratic invariants of switched systems

Abstract : We present a new numerical abstract domain based on ellipsoids 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 difficulty that ellipsoids do not have a lattice structure by exhibiting a canonical operator overapproximating the union. This operator is the only one that permits the performance of analyses that are invariant with respect to a linear transformation of state variables. It provides the minimum volume ellipsoid enclosing two given ellipsoids. We show that it can be computed in O(n3) elementary algebraic operations. We finally develop a fast nonlinear power-type algorithm, which allows one to determine 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 benchmarks, 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 : Saturday, December 31, 2016 - 1:03:32 PM
Last modification on : Friday, April 30, 2021 - 10:03:54 AM



Xavier Allamigeon, Stéphane Gaubert, Eric Goubault, Sylvie Putot, Nikolas Stott. A scalable algebraic method to infer quadratic invariants of switched systems. ACM Transactions on Embedded Computing Systems (TECS), ACM, 2016, Special Issue on ESWEEK2015, 15 (4), ⟨10.1145/2932187⟩. ⟨hal-01423744⟩



Record views