Skip to Main content Skip to Navigation
Conference papers

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
Inria Saclay - Ile de France, CMAP - Centre de Mathématiques Appliquées - Ecole Polytechnique
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.
Document type :
Conference papers
Complete list of metadata
https://hal.inria.fr/hal-01249320
Contributor : Stephane Gaubert <>
Submitted on : Thursday, December 31, 2015 - 3:06:17 PM
Last modification on : Tuesday, December 8, 2020 - 9:45:37 AM

Identifiers

Collections

CNRS | X | INSMI | X-CMAP | CMAP | INRIA | CEA | TDS-MACS | 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), Alain Girault, INRIA, Grenoble, France and Nan Guan, Northeastern University, China, Oct 2015, Amsterdam, Netherlands. ⟨10.1109/EMSOFT.2015.7318262⟩. ⟨hal-01249320⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

602

 

Contact                    Legal Notice                    Personal Data