A hybrid barrier certificate approach to satisfy linear temporal logic specifications

20 April 2018
20 April 2018
DII - Dipartimento di Ingegneria Industriale
via Sommarive, 9 - 38123 Povo, Trento
+39 0461 282500 - 2503
fax +39 0461 281977

Venue: Seminar Room, h. 11:00 – 12:00 , Polo scientifico-tecnologico Fabio Ferrari – via Sommarive 9 - Trento

  • Andrea Bisoffi,  KTH Royal Institute of Technology, Sweden

Abstract: Linear temporal logic allows to formulate richly expressive control specifications for continuous-time plants as, for instance, high-level tasks for multi-robot systems. The problem of satisfying such a linear temporal logic specification on a physical plant is formulated using hybrid dynamical systems. The satisfaction of the considered temporal logic specification is equivalent to a so-called eventuality property for the logical states of the hybrid system. In order to solve the problem, we first characterize eventuality for that hybrid system framework, and extend to it barrier certificates, which allow to check eventuality without explicitly analyzing solutions. We relate eventuality and the existence of hybrid barrier certificates through necessary and sufficient conditions. Then, we propose a solution to the original problem in terms of a hybrid barrier certificate. The proposed method is illustrated on a numerical example.

Biosketch: Andrea Bisoffi received his M.Sc. cum laude in Automatic Control Engineering from Politecnico di Milano, Italy, in 2013 and his Ph.D. in Mechatronics from the University of Trento, Italy, in 2017. In 2015–2016 he was a visiting scholar in the Control Group at the University of Cambridge, UK. He is currently a Post-doc at KTH Royal Institute of Technology, Sweden. His current research interests include hybrid and nonlinear control systems, with applications to mechanical, automotive and multi-robot systems.