Deriving Liveness Properties of Hybrid Systems from Reachable Sets and Lyapunov-Like Certificates

In this paper we tackle the problem of proving generic LTL properties of hybrid systems with a particular focus on liveness properties such as recurrence of regions, response to stimuli, or region stability. Although many advances have been made in the analysis of reachability and safety properties of dynamic and hybrid systems, there is a lack of tool support for the automated verification of liveness properties. We propose a fully automated approach that combines Lyapunov synthesis, reachability analysis, and SMT-based quantifier elimination to build a discrete abstraction and then applies standard model checking algorithms. A key step of the algorithm is the derivation of LTL constraints from reachable sets computations and Lyapunov-like certificates. We implemented the approach on top of the CORA and nuXmv tools and show how it can scale in the size of the discrete structure and how it can prove properties over linear and non-linear complex dynamics.