Frédéric Viry : Reachability of high-dimensional dynamical systems through low-dimensional projections

De Ensiwiki
Aller à : navigation, rechercher

Travail de recherche effectué au laboratoire Verimag, sous la direction de Goran Frehse (maître de conférences) et de Marcelo Forets (post-doctorant).

Introduction

Contexte Industriel

Tous les jours, nous manipulons des systèmes très complexes (téléphone, voiture, train... etc). Comment être sûrs de leur bon fonctionnement ? Sous quelles conditions fonctionnent-ils ? Ces questions peuvent être éludées dans certains cas, mais leurs réponses peut être critiques dans d'autres, notamment dans l'automobile, en aéronautique ou dans l'énergie.

Pour cela, plusieurs solutions sont offertes :

- Le test : coûteux car nécessite un prototype, peut être dangereux pour l'Homme et son environnement

- La simulation : peu coûteux mais non exhaustive, tous les cas ne sont pas couverts

- La vérification formelle : cher en temps de calcul et problème généralement difficile, mais exhaustif

Nous allons ici nous intéresser à la vérification formelle. C'est un sujet d'actualité dans la recherche académique. Elle consiste en, au lieu de traiter des cas particuliers (simulations), raisonner sur des ensembles de cas possibles.

Atteignabilité des Systèmes Affines

Nous nous intéressons ici à l'atteignabilité des systèmes affines à composante indéterministe. Ils sont assez simples pour être étudiés relativement facilement, et assez complexes pour des applications industrielles. Ce sont des systèmes dynamiques définis de la manière suivante :


\dot{x} = Ax + Bu

x est l'état du système, A et B sont des matrices, et u est une fonction à valeurs dans \mathcal{U} un ensemble compact et convexe. On appelle \mathcal{X}_0 l'ensemble des états initiaux du système.

Ces systèmes peuvent par exemple décrire les valeurs d'une fonction sur un maillage décrite par une EDP, grâce à un schéma aux différences finies, où l'ensemble \mathcal{U} permet de tenir compte de l'erreur de discrétisation.

Travail Réalisé

Le but de l'atteignabilité est de calculer ou d'approximer l'ensembles des états atteignables du système pour un ensemble de conditions initiales \mathcal{X}_0 et un ensemble d'entrées possible \mathcal{U}.

Etat de l'Art

On se place dans l'espace vectoriel E = \mathbb{R}^n muni d'une norme \Vert \cdot \Vert. Il a été montré (thèse de Colas Le Guernic, 2009) que l'atteignabilité d'un système affine continu peut se réduire à l'atteignabilité d'un système affine discret, pour un pas de discrétisation \delta > 0 donné:


\begin{cases}
\Omega_{k+1} = e^{\delta A}\Omega_k \oplus \delta B \mathcal{U} \oplus \beta_\delta \mathcal{B} \\
\Omega_0 = \text{CH}(\mathcal{X}_0, e^{\delta A}\mathcal{X}_0 \oplus \delta B \mathcal{U} \oplus \alpha_\delta \mathcal{B})
\end{cases}

\mathcal{B} désigne la boule unité pour la norme donnée, \alpha_\delta et \beta_\delta sont des facteurs de grossissement.

L'union de N-1 de ces ensembles permet de surapproximer les états atteignables du système sur l'intervalle de temps [0, N\delta]. La figure suivante montre en bleu l'ensemble des états initiaux, en noir l'ensemble des états atteignables, et en rouge la surapproximation.

Reach.png

Concrètement, ces ensembles sont à leur tour surapproximés par des polyèdres, car ils sont en général très complexes. Ces polyèdres sont calculés par le biais de fonction supports[1].

Problème

Dans les applications industrielles, les systèmes étudiés sont généralement de haute dimension (espace d'états de dimension 100 par exemple). De très hautes dimensions peuvent être atteintes dans le cas de discrétisation spatiales d'EDP (milliers de dimensions) ! Les méthodes actuelles ne sont actuellement pas capable de gérer ce type de cas, les ensembles à considérer étant trop complexes.

Idée

Un groupe de chercheurs du laboratoire Verimag ainsi que de l'Université de Freiburg (Allemagne) ont trouvé une méthode pour casser la complexité de ce problème. L'idée est qu'une fois le système discrétisé dans le temps, il est possible de décomposer ce système discret en sous-systèmes de plus petite dimension, grâce à des projections. Cela est très intéressant car l'opération de projection coûte peu cher avec les fonctions support.

On note P une partition des n variables d'états du système en b sous-ensembles. P_i est donc un ensemble de variables. On note \pi_i l'opération de projection sur les variables sélectionnées par P_i. On note \Phi = e^{\delta A}.

La matrice \Phi se décompose en :


\Phi =
            \begin{pmatrix}
                \Phi_{1,1} & \cdots & \Phi_{1,b}\\
                \vdots & \ddots & \vdots\\
                \Phi_{b,1} & \cdots & \Phi_{b,b}
            \end{pmatrix}

Nous allons projeter nos ensembles sur des sous-espaces de petite dimension, faire les calculs d'atteignabilité en petite dimension, puis rassembler ces résultats par un produit cartésien. On note \widehat{\Omega}_k le produit cartésien des projections de \Omega_k sur chacun des ensembles de variables P_i. L'image suivante illustre le procédé :

Deco.png

Ainsi, notre relation de récurrence précédente se réécrit :


\widehat{\Omega}_{k+1}^{(i)} = \bigoplus\limits_{j=1}^b \Phi_{i,j}
            \widehat{\Omega}_{k}^{(j)} \oplus \delta \pi_i(B \mathcal{U}) \oplus
            \beta_\delta \pi_i(\mathcal{B}), \quad \forall i \in \{1, \cdots, b\}

Il est possible d'exprimer facilement ces ensembles par le biais de fonctions support et ainsi de les approximer.

Cependant, comme illustré dans l'image précédente, ces projections induisent une erreur incontrôlable. A cause de la formule de récurrence, cette erreur peut s'amplifier. C'est ce que l'on appelle l'effet d'emballage. Nous verrons dans des exemples pratiques cet effet.

Résultats

La méthode a été implémentée en langage Julia. Voyons ici si elle fonctionne correctement sur un exemple simple en 4 dimensions.

Une boule de masse 1kg est lancé depuis le haut d'une tour de 100m à une vitesse initiale horizontale de 5m/s. Ma voiture est garée dans la rue 15m plus loin. La boule va-t-elle impacter la voiture ?

Ce problème est un problème très simple d'atteignabilité. Le système affine associé est le suivant :


\begin{pmatrix} \dot{x}_1 \\ \dot{v}_1 \\ \dot{x}_2 \\ \dot{v}_2
            \end{pmatrix} = \begin{pmatrix} 0 & 1 & 0 & 0 \\ 0 & 0 & 0 & 0 \\
            0 & 0 & 0 & 1 \\ 0 & 0 & 0 & 0
            \end{pmatrix} \begin{pmatrix} x_1 \\ v_1 \\ x_2 \\ v_2
            \end{pmatrix} + \begin{pmatrix} 0 \\ 0 \\ 0 \\ -g
            \end{pmatrix}

x_1, x_2 sont les coordonnées de la boule dans un plan vertical, v_1, v_2 sont les coordonnées de la vitesse, et g est l'accélération de pesanteur.

Le résultat est le suivant : aucune trajectoire n'indique que la boule tombera sur la voiture.

Proj motion method car.png

Voici le résultat donné par SpaceEx, logiciel spécialisé développé au laboratoire Verimag :

Proj motion spaceex car.png

Nous obtenons des résultats très proches. Sur cet exemple, la méthode fonctionne donc correctement, il n'y a pas d'accumulation d'erreur.

Voici un exemple où la méthode est mise à défaut : ici, assurer une certaine borne d'erreur rend les calculs beaucoup trop longs. Nous tentons alors de faire nos calculs avec une plus grand erreur admise. L'erreur s'accumule et le résultat devient totalement inexploitable.

Résultat de la méthode :

Crane method.png

Résultat attendu (SpaceEx) :

Crane spaceex.png

Conclusion

Finalement, nous avons pu développer une méthode qui fonctionne dans certains cas. Cependant elle manque de précision. Une piste n'a pas été explorée durant ce stage, qui utilise une formule non récurrente. Elle pourra être exploitée dans de futurs travaux et régler le problème d'effet d'emballage.

Références

[1] Matthias Althoff and Goran Frehse, Combining Zonotopes and Support Functions for Efficient Reachability Analysis of Linear Systems, Decision and Control (CDC), 2016 IEEE 55th Conference on, IEEE, 2016, pp. 7439-7446.

[2] Athanasios C. Antoulas, Danny C. Sorensen, and Serkan Gugercin, A Survey of Model Reduction Methods for Large-Scale Systems, Contemporary Mathematics 280 (2001), 193-220

[3] Jeff Bezanson, Alan Edelman, Stefan Karpinski, and Viral B. Shah, Julia: A Fresh Approach to Numerical Computing, SIAM Review 59 (2017).

[4] Sergiy Bogomolov, Marcelo Forets, Goran Frehse, Andreas Podelski, Christian Schilling, and Frédéric Viry, Decomposing Reachability Computations for Affine Systems, (under submission) (2017).

[5] Mo Chen, Sylvia L. Herbert, Mahesh S. Vashishtha, Somil Bansal, and Claire J. Tomlin, Decomposition of Reachable Sets and Tubes for a Class of Nonlinear Systems, arXiv preprint arXiv:1611.00122 (2016).

[6] Zhi Han and Bruce H. Krogh, Reachability Analysis of Large-Scale Affine Systems using Low-Dimensional Polytopes, HSCC, 2006, pp. 287-301.

[7] Shahab Kaynama and Meeko Oishi, Schur-based Decomposition for Reachability Analysis of Linear Time-Invariant Systems, Decision and Control, 2009 held jointly with the 2009 28th Chinese Control Conference. CDC/CCC 2009. Proceedings of the 48th IEEE Conference on, IEEE, 2009, pp. 69-74.

[8] Shahab Kaynama and Meeko Oishi, Overapproximating the Reachable Sets of LTI Systems through a Similarity Transformation, ACC, 2010, pp. 1874-1879.

[9] Shahab Kaynama and Meeko Oishi, Complexity Reduction through a Schur-based Decomposition for Reachability Analyse of Linear Time-Invariant Systems, International Journal of Control 84 (2011), no. 1, 165-179.

[10] Colas Le Guernic, Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics, Ph. D. thesis, Université Joseph Fourier, 2009.

[11] Colas Le Guernic and Antoine Girard, Reachability Analysis of Linear Systems using Support Functions, Elsevier (2010).

[12] Alexander V. Lotov, Vladimir A. Bushenkov, and Georgy K. Kamenev, Interactive Decision Maps, Applied Optimization, vol. 89, Kluwer, 2004.

[13] Alexander V. Lotov and Alexis I. Pospelov, The Modified Method of Refined Bounds for Polyhedral Approximation of Convex Polytopes, Zhurnal Vychislitel'noi Matematiki i Matematicheskoi Fiziki (2007).

[14] Hoang-Dung Tran, Luan Viet Nguyen, Weiming Xiang, and Taylor T. Johnson, Order-reduction Abstractions for Satefy Verification of High-Dimensional Linear Systems, CoRR abs/1602.06417 (2016).

[15] Frédéric Viry, Planar Projections of Polyhedra in High Dimension, Tech. Report, Université Grenoble Alpes, 2016.

Rapport

Télécharger le rapport ici : [2]

Télécharger les slides ici : [3]