Système hybride - Hybrid system

Un système hybride est un système dynamique qui présente à la fois un comportement dynamique continu et discret - un système qui peut à la fois s'écouler (décrit par une équation différentielle ) et sauter (décrit par une machine à états ou un automate ). Souvent, le terme «système dynamique hybride» est utilisé pour distinguer les systèmes hybrides tels que ceux qui combinent les réseaux neuronaux et la logique floue , ou les transmissions électriques et mécaniques. Un système hybride a l'avantage d'englober une plus grande classe de systèmes dans sa structure, ce qui permet une plus grande flexibilité dans la modélisation des phénomènes dynamiques.

En général, l' état d'un système hybride est défini par les valeurs des variables continues et un mode discret . L'état change soit en continu, selon une condition d' écoulement , soit discrètement selon un graphe de contrôle . Un écoulement continu est autorisé tant que les soi-disant invariants sont maintenus, tandis que des transitions discrètes peuvent se produire dès que des conditions de saut données sont satisfaites. Des transitions discrètes peuvent être associées à des événements .

Exemples

Les systèmes hybrides ont été utilisés pour modéliser plusieurs systèmes cyber-physiques, y compris des systèmes physiques avec impact , des contrôleurs logico-dynamiques et même une congestion Internet .

Balle rebondissante

Un exemple canonique d'un système hybride est la balle rebondissante , un système physique avec impact. Ici, la balle (considérée comme une masse ponctuelle) est lâchée d'une hauteur initiale et rebondit sur le sol, dissipant son énergie à chaque rebond. La balle présente une dynamique continue entre chaque rebond; cependant, lorsque la balle heurte le sol, sa vitesse subit un changement discret modélisé après une collision inélastique . Une description mathématique de la balle qui rebondit suit. Soit la hauteur de la balle et la vitesse de la balle. Un système hybride décrivant le ballon est le suivant: ${\ displaystyle x_ {1}}$ ${\ displaystyle x_ {2}}$

Quand , le débit est régi par , où est l'accélération due à la gravité. Ces équations indiquent que lorsque la balle est au-dessus du sol, elle est attirée vers le sol par gravité. ${\ displaystyle x \ in C = \ {x_ {1}> 0 \}}$ ${\ displaystyle {\ dot {x}} _ {1} = x_ {2}, {\ dot {x}} _ {2} = - g}$ ${\ displaystyle g}$

Quand , les sauts sont régis par , où est un facteur de dissipation. Cela veut dire que lorsque la hauteur de la balle est nulle (elle a heurté le sol), sa vitesse est inversée et diminuée d'un facteur de . En fait, cela décrit la nature de la collision inélastique. ${\ displaystyle x \ in D = \ {x_ {1} = 0 \}}$ ${\ displaystyle x_ {1} ^ {+} = x_ {1}, x_ {2} ^ {+} = - \ gamma x_ {2}}$ ${\ displaystyle 0 <\ gamma <1}$ ${\ displaystyle \ gamma}$

La balle rebondissante est un système hybride particulièrement intéressant, car elle présente un comportement Zeno . Le comportement de Zeno a une définition mathématique stricte, mais peut être décrit de manière informelle comme le système effectuant un nombre infini de sauts dans un laps de temps fini . Dans cet exemple, chaque fois que la balle rebondit, elle perd de l'énergie, ce qui rapproche de plus en plus les sauts suivants (impact avec le sol) dans le temps.

Il est à noter que le modèle dynamique est complet si et seulement si on ajoute la force de contact entre le sol et la balle. En effet, sans forces, on ne peut pas définir correctement la balle qui rebondit et le modèle est, d'un point de vue mécanique, dénué de sens. Le modèle de contact le plus simple qui représente les interactions entre la balle et le sol est la relation de complémentarité entre la force et la distance (l'écart) entre la balle et le sol. Ceci est écrit comme un tel modèle de contact n'intègre pas de forces magnétiques, ni d'effets de collage. Lorsque les relations de complémentarité sont en place, on peut continuer à intégrer le système après que les impacts se sont accumulés et disparus: l'équilibre du système est bien défini comme l'équilibre statique de la balle au sol, sous l'action de la pesanteur compensée par la force de contact . On remarque également à partir de l'analyse convexe de base que la relation de complémentarité peut être réécrite de manière équivalente comme l'inclusion dans un cône normal, de sorte que la dynamique de la balle rebondissante est une inclusion différentielle dans un cône normal à un ensemble convexe. Voir les chapitres 1, 2 et 3 du livre d'Acary-Brogliato cité ci-dessous (Springer LNACM 35, 2008). Voir aussi les autres références sur la mécanique non lisse. ${\ displaystyle 0 \ leq \ lambda \ perp x_ {1} \ geq 0.}$ ${\ displaystyle \ lambda}$

Vérification des systèmes hybrides

Il existe des approches pour prouver automatiquement les propriétés des systèmes hybrides (par exemple, certains des outils mentionnés ci-dessous). Les techniques courantes pour prouver la sécurité des systèmes hybrides sont le calcul d'ensembles accessibles, le raffinement d'abstraction et les certificats de barrière .

La plupart des tâches de vérification sont indécidables, ce qui rend les algorithmes de vérification généraux impossibles. Au lieu de cela, les outils sont analysés pour leurs capacités sur les problèmes de référence. Une caractérisation théorique possible de ceci est des algorithmes qui réussissent avec la vérification des systèmes hybrides dans tous les cas robustes, ce qui implique que de nombreux problèmes pour les systèmes hybrides, bien qu'indécidables, sont au moins quasi-décidables.

Autres approches de modélisation

Deux approches de base de la modélisation de systèmes hybrides peuvent être classées, une implicite et une explicite. L'approche explicite est souvent représentée par un automate hybride , un programme hybride ou un réseau de Petri hybride . L'approche implicite est souvent représentée par des équations gardées pour aboutir à des systèmes d' équations algébriques différentielles (DAE) où les équations actives peuvent changer, par exemple au moyen d'un graphe de liaison hybride .

En tant qu'approche de simulation unifiée pour l'analyse de systèmes hybrides, il existe une méthode basée sur le formalisme DEVS dans lequel les intégrateurs d'équations différentielles sont quantifiés en modèles DEVS atomiques . Ces méthodes génèrent des traces des comportements du système à la manière d'un système d'événements discrets qui sont différents des systèmes temporels discrets. Les détails de cette approche peuvent être trouvés dans les références [Kofman2004] [CF2006] [Nutaro2010] et l'outil logiciel PowerDEVS .

Outils

Ariadne : une bibliothèque C ++ pour l'analyse d'accessibilité (numériquement rigoureuse) des systèmes hybrides non linéaires
C2E2 : Vérificateur de système hybride non linéaire
CORA : une boîte à outils MATLAB pour l'analyse d'accessibilité des systèmes cyber-physiques, y compris les systèmes hybrides
Flow * : Un outil d'analyse d'accessibilité des systèmes hybrides non linéaires
HyCreate : un outil de surapproximation de l'accessibilité des automates hybrides
HyEQ : un solveur de système hybride pour Matlab
HyPro : une bibliothèque C ++ pour les représentations d'ensembles d'états pour l'analyse d'accessibilité des systèmes hybrides
HSolver : vérification des systèmes hybrides
HyTech : un vérificateur de modèle pour les systèmes hybrides
JuliaReach : une boîte à outils pour l' accessibilité basée sur les ensembles
KeYmaera : un prouveur de théorème hybride pour les systèmes hybrides
PHAVer : Vérificateur d' automates hybrides polyédriques
PowerDEVS : Un outil logiciel polyvalent de modélisation et de simulation DEVS orienté vers la simulation de systèmes hybrides
SCOTS : un outil de synthèse de contrôleurs corrects à la construction pour les systèmes hybrides
SpaceEx : Explorateur d'espace d'état
S-TaLiRo : une boîte à outils MATLAB pour la vérification des systèmes hybrides par rapport aux spécifications de la logique temporelle

Voir également

Lectures complémentaires

Henzinger, Thomas A. (1996), "The Theory of Hybrid Automata", 11th Annual Symposium on Logic in Computer Science (LICS) , IEEE Computer Society Press, pp. 278–292, archivé de l'original le 2010-01-27
Alur, Rajeev; Courcoubetis, Costas; Halbwachs, Nicolas; Henzinger, Thomas A .; Ho, Pei-Hsin; Nicollin, Xavier; Olivero, Alfredo; Sifakis, Joseph; Yovine, Sergio (1995), "L'analyse algorithmique des systèmes hybrides" , Theoretical Computer Science , 138 (1): 3–34, doi : 10.1016 / 0304-3975 (94) 00202-T , hdl : 1813/6241 , archivé à partir de l'original sur 27/01/2010
Goebel, Rafal; Sanfelice, Ricardo G .; Teel, Andrew R. (2009), «Hybrid dynamical systems», IEEE Control Systems Magazine , 29 (2): 28–93, doi : 10.1109 / MCS.2008.931718 , S2CID 46488751
Acary, Vincent; Brogliato, Bernard (2008), «Numerical Methods for Nonsmooth Dynamical Systems», Notes de cours en mécanique appliquée et computationnelle , 35
[Kofman2004] Kofman, E (2004), «Discrete Event Simulation of Hybrid Systems», SIAM Journal on Scientific Computing , 25 (5): 1771–1797, CiteSeerX 10.1.1.72.2475 , doi : 10.1137 / S1064827502418379
[CF2006] Francois E. Cellier et Ernesto Kofman (2006), Continuous System Simulation (première éd.), Springer, ISBN 978-0-387-26102-7
[Nutaro2010] James Nutaro (2010), Création de logiciels pour la simulation: théorie, algorithmes et applications en C ++ (première éd.), Wiley
Brogliato, Bernard; Tanwani, Aneel (2020), «Systèmes dynamiques couplés à des opérateurs à valeurs d'ensemble monotones: formalismes, applications, bonne position et stabilité» (PDF) , SIAM Review , 62 (1): 3–129, doi : 10.1137 / 18M1234795

Liens externes

Comité CSS IEEE sur les systèmes hybrides

Languages

In other projects