Nicolas Markey

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.

@inproceedings{formats2015-BMPS,
  author =              {Bouyer, Patricia and Markey, Nicolas and Perrin,
                         Nicolas and Schlehuber{-}Caissier, Philipp},
  title =               {Timed automata abstraction of switched dynamical
                         systems using control funnels},
  editor =              {Sankaranarayanan, Sriram and Vicario, Enrico},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'15)},
  acronym =             {{FORMATS}'15},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9268},
  pages =               {60-75},
  year =                {2015},
  month =               sep,
  doi =                 {10.1007/978-3-319-22975-1_5},
  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~\emph{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.},
}