Ivanova, Elena
[Author]
;
université Paris-Saclay
[Contributor];
Girard, Antoine
[Contributor]
Efficient Synthesis of Safety Controllers using Symbolic Models and Lazy Algorithms ; Synthèse efficace des contrôleurs de sécurité à l'aide de modèles symboliques et d'algorithmes paresseux
You can manage bookmarks using lists, please log in to your user account for this.
Media type:
Text;
E-Book;
Electronic Thesis
Title:
Efficient Synthesis of Safety Controllers using Symbolic Models and Lazy Algorithms ; Synthèse efficace des contrôleurs de sécurité à l'aide de modèles symboliques et d'algorithmes paresseux
Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
Cette thèse porte sur le développement d'approches efficaces de synthèse de contrôleurs basées sur l'abstraction pour les systèmes cyber-physiques (CPS). Alors que les méthodes basées sur l'abstraction pour la conception de CPS ont fait l'objet de recherches intensives au cours des dernières décennies, l'évolutivité de ces techniques reste un problème. Cette thèse se concentre sur le développement d'algorithmes de synthèse paresseuse pour les spécifications de sécurité. Les spécifications de sécurité consistent à maintenir la trajectoire du système à l'intérieur d'un ensemble sûr donné. Cette spécification est de la plus haute importance dans de nombreux problèmes d'ingénierie, souvent prioritaires par rapport à d'autres exigences de performance. Les approches paresseuses surpassent l'algorithme de synthèse classique [Tabuada, 2009] en évitant les calculs, qui ne sont pas essentiels pour les objectifs de synthèse. Le chapitre 1 motive la thèse et présente l'état de l'art. Le chapitre 2 structure les approches de synthèse paresseuses existantes et met l'accent sur trois sources d'efficacité : les informations sur les états contrôlables a priori, les priorités sur les entrées et les états non accessibles à partir de l'ensemble initial. Le chapitre 3 propose un algorithme, qui explore itérativement les états à la frontière du domaine contrôlable tout en évitant l'exploration des états internes, en supposant qu'ils sont contrôlables en toute sécurité a priori. Un contrôleur de sécurité en boucle fermée pour le problème d'origine est alors défini comme suit : nous utilisons le contrôleur abstrait pour repousser le système d'un état limite vers l'intérieur, tandis que pour les états internes, toute entrée admissible est valide. Le chapitre 4 présente un algorithme qui restreint les calculs de synthèse du contrôleur aux seuls états atteignables tout en privilégiant les transitions de plus longue durée. Le système original est abstrait par un modèle symbolique avec une grille adaptative. De plus, un nouveau type ...