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.
Type de document :
Article dans une revue
ACM Transactions on Embedded Computing Systems (TECS), ACM, 2016, Special Issue on ESWEEK2015, 15 (4), 〈10.1145/2932187〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01423744
Contributeur : Stephane Gaubert <>
Soumis le : samedi 31 décembre 2016 - 13:03:32
Dernière modification le : jeudi 11 janvier 2018 - 06:22:34

Identifiants

Citation

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〉

Partager

Métriques

Consultations de la notice

440