Authors: Battista Ludovico, Stefano Tonetta, Gianni Zampedri
(to be) Presented at TACAS26
The automated verification of Linear Temporal Logic (LTL) properties over hybrid systems is an important challenge in formal methods. While numerous tools exist for checking safety and reachability, no framework currently provides a concrete language and algorithm for the full verification of LTL on hybrid models that combine discrete and continuous dynamics described in terms of differential equations. We present VeriLHyS, the first tool that enables the specification and automated verification of LTL properties for hybrid automata. The framework integrates continuous analysis techniques with symbolic model checking, leveraging Lyapunov-like, descent, and barrier certificates, as well as reachability set overapproximations, to derive sound LTL constraints on the system abstraction. These constraints are then checked using symbolic LTL model checking, ensuring correctness of the verified property on the original hybrid system. VeriLHyS supports both linear and nonlinear dynamics and is built on top of existing engines such as CORA, nuxmv, and SMT solvers. Our experiments show that it can handle complex hybrid benchmarks that go beyond the reach of existing tools.
The code that accompanies this paper has undergone an evaluation receiving the Available, Functional, and Reusable badges.