A scalable algebraic method to infer quadratic invariants of switched systems

Xavier Allamigeon 1, 2 Stéphane Gaubert 2, 1 Eric Goubault 3 Sylvie Putot 3 Nikolas Stott 1, 2
1 CMAP - Centre de Mathématiques Appliquées - Ecole Polytechnique
2 MAXPLUS - Max-plus algebras and mathematics of decision
CMAP - Centre de Mathématiques Appliquées - Ecole Polytechnique, Inria Saclay - Ile de France
3 LIST - Laboratoire d'Intégration des Systèmes et des Technologies
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.
Type de document :
Communication dans un congrès
International Conference on Embedded Software (EMSOFT'2015), Oct 2015, Amsterdam, Netherlands. International Conference on Embedded Software (EMSOFT'2015), 2015, International Conference on Embedded Software (EMSOFT'2015). 〈IEEE〉. 〈10.1109/EMSOFT.2015.7318262〉
Liste complète des métadonnées
https://hal.inria.fr/hal-01249320
Contributeur : Stephane Gaubert <>
Soumis le : jeudi 31 décembre 2015 - 15:06:17
Dernière modification le : mercredi 14 novembre 2018 - 15:20:11

Identifiants

Collections

X | INSMI | X-CMAP | CMAP | INRIA | PARISTECH | CEA | TDS-MACS | UNIV-PARIS-SACLAY | CEA-UPSAY | DRT | LIST | X-DEP-MATHA

Citation

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), Oct 2015, Amsterdam, Netherlands. International Conference on Embedded Software (EMSOFT'2015), 2015, International Conference on Embedded Software (EMSOFT'2015). 〈IEEE〉. 〈10.1109/EMSOFT.2015.7318262〉. 〈hal-01249320〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

422

Contact


archive-ouverte@inria.fr