Timed-automata abstraction of switched dynamical systems using control invariants - Sorbonne Université Accéder directement au contenu
Article Dans Une Revue Real-Time Systems Année : 2017

Timed-automata abstraction of switched dynamical systems using control invariants

Résumé

The development of formal methods for control design is an important challenge with potential applications in a wide range of safety-critical cyber-physical systems. Focusing on switched dynamical systems, we propose a new abstraction, based on time-varying regions of invariance (control funnels), that models behaviors of systems as timed automata. The main advantage of this method is that it allows for the automated verification and reactive controller synthesis without discretizing the evolution of the state of the system. Efficient and analytic constructions are possible in the case of linear dynamics whereas bounding funnels with conjectured properties based on numerical simulations can be used for general nonlinear dynamics. We demonstrate the potential of our approach with three examples.
Fichier principal
Vignette du fichier
Bouyer_2017_Timed-automata.pdf (2.71 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01436413 , version 1 (16-01-2017)

Identifiants

Citer

Patricia Bouyer, Nicolas Markey, Nicolas Perrin, Philipp Schlehuber-Caissier. Timed-automata abstraction of switched dynamical systems using control invariants. Real-Time Systems, 2017, pp.1-27. ⟨10.1007/s11241-016-9262-3⟩. ⟨hal-01436413⟩
281 Consultations
232 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More