Skip to Main content Skip to Navigation
Book sections

Timed-Automata Abstraction of Switched Dynamical Systems Using Control Funnels

Abstract : 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 (the control funnels), that models behaviors of systems as timed automata. The main advantage of this method is that it allows automated verification of formal specifications and reactive controller synthesis without discretizing the evolution of the state of the system. Efficient constructions are possible in the case of linear dynamics. We demonstrate the potential of our approach with two examples.
Document type :
Book sections
Complete list of metadatas

Cited literature [25 references]  Display  Hide  Download

https://hal.sorbonne-universite.fr/hal-01395104
Contributor : Gestionnaire Hal-Upmc <>
Submitted on : Thursday, November 10, 2016 - 2:31:46 PM
Last modification on : Monday, February 15, 2021 - 10:49:08 AM
Long-term archiving on: : Wednesday, March 15, 2017 - 3:41:36 AM

File

Bouyer_2015_Timed-Automata.pdf
Files produced by the author(s)

Identifiers

Citation

Patricia Bouyer, Nicolas Markey, Nicolas Perrin, Philipp Schlehuber-Caissier. Timed-Automata Abstraction of Switched Dynamical Systems Using Control Funnels. Formal Modeling and Analysis of Timed Systems, 9268, Springer International Publishing, pp.60 - 75, 2015, Lecture Notes in Computer Science, 978-3-319-22974-4. ⟨10.1007/978-3-319-22975-1_5⟩. ⟨hal-01395104⟩

Share

Metrics

Record views

671

Files downloads

296