Authors: Battista Ludovico, Stefano Tonetta
(to be) Presented at ATVA25
In this paper we tackle the problem of proving generic LTL properties of hybrid systems with a particular focus on liveness proper- ties 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 synthe- sis, reachability analysis and SMT-based quantifier elimination to build a discrete abstraction and then applies standard model checking algo- rithms. A key step of the algorithm is the derivation of LTL constraints from reachable sets computations and Lyapunov-like certificates. We im- plemented 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.