A hybrid barrier certificate approach to satisfy linear temporal logic specifications
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.