CTL
7 décembre 2012 - 14h00
Reachability analysis of nonlinear dynamical systems (Phd Defense)
par Romain Testylier de UJF
Abstract: This thesis is concerned with safety verification of hybrid systems, which are a common mathematical model for describing systems integrating both continuous and discrete dynamics. They found applications in various domains such that embedded systems and biological systems.
Besides the undecidability of the verification problem for even hybrid systems with simple dynamics, the main difficulty in applying the standard approaches (which have been successful for hardware and software verification) is the lack of efficient methods for computing or approximating the trajectory sets generated by their continuous dynamics (described by differential equations). While many properties of linear systems allowed to develop efficient reachability methods, non-linear systems remain a challenge. In this thesis we focus on the problem of over-approximating the reachable states of hybrid systems with non-linear continuous dynamics.
First, we present a new method for finding good approximation domains for the hybridization method, which is a systematic method for computing a piecewise-linear approximation of the non-linear system. Then, we present a new reachability technique for polynomial systems, based on the Bernstein expansion. We next present some mechanisms to improve the precision of polyhedron-based reachability analysis by adding redundant constraints to the description of the reachable set. Finally, we describe a prototype tool in which we implemented the proposed algorithms and our experimental results obtained using the tool for a number of case studies.
Jury:
- Thao Dang, Chargée de Recherche, VERIMAG/CNRS, Directrice de thèse
- Eric Goubault, Directeur de Recherche, CEA, Rapporteur
- Erika Abraham, Professeur, Aachen University, Rapporteur
- Olivier Bournez, Professeur, Ecole Polytechnique, Examinateur
- Carla Piazza, Professeur, Udine University, Examinatrice
- Bertrand Jeannet, Chargé de Recherche, INRIA, Examinateur
