Auditorium (IMAG)
16 May 2018 - 14h00
A Calculus of Complex Zonotopes for Computing Invariants of Affine Hybrid Systems (Phd Defense)
by Arvind Adimoolam from VERIMAG
Abstract: Computing reachable sets is a de facto approach used in many formal verification methods for hybrid systems. But exact computation of the reachable set is an intractable problem for many kinds of hybrid systems, either due to undecidability or high computational complexity. Alternatively, quite a lot of research has been focused on using set representations that can be efficiently manipulated to compute sufficiently accurate over-approximation of the reachable set. Zonotopes are a useful set representation in reachability analysis because of their closure and low complexity for computing linear transformation and Minkowski sum operations. But for approximating the unbounded time reachable sets by positive invariants, zonotopes have the following drawback. The effectiveness of a set representation for computing a positive invariant depends on efficiently encoding the directions for convergence of the states to an equilibrium. In an affine hybrid system, some of the directions for convergence can be encoded by the complex valued eigenvectors of the transformation matrices. But the zonotope representation can not exploit the complex eigenstructure of the transformation matrices because it only has real valued generators.
Therefore, we extend real zonotopes to the complex valued domain in a way that can capture contraction along complex valued vectors. This yields a new set representation called complex zonotope. Geometrically, complex zonotopes represent a wider class of sets that include some non-polytopic sets as well as polytopic zonotopes. They retain the merit of real zonotopes that we can efficiently perform linear transformation and Minkowski sum operations and compute the support function. Additionally, we show that they can capture contraction along complex valued eigenvectors. Furthermore, we develop computationally tractable approximations for inclusion-checking and intersection with half-spaces. Using these set operations on complex zonotopes, we develop convex programs to verify linear invariance properties of discrete time affine hybrid systems and exponential stability of linear impulsive systems. Our experiments on some benchmark examples demonstrate the efficiency of the verification techniques based on complex zonotopes.
Slides of the Presentation.
Jury:
Dr. Thao Dang - Directeur de these, VERIMAG, Grenoble.
Prof. Sylvie Putot - Rapporteur, Ecole Polytechnique.
Prof. Mahesh Viswanathan - Rapporteur, University of Illinois at Urbana Champaign, USA.
Prof. Luc Jaulin - University Bretagne Occidentale, Examinateur.
Prof. Laurent Fribourg - Examinateur, ENS Cachan.
