HyLTL: a temporal logic for model checking hybrid systems

TL;DR

HyLTL is a new temporal logic designed for specifying complex properties of hybrid systems, enabling model checking by translating formulas into hybrid automata and reducing the problem to reachability analysis.

Contribution

The paper introduces HyLTL, a logic that allows for model checking of hybrid systems with complex properties, bridging the gap between continuous dynamics and verification.

Findings

Model checking for hybrid systems can be reduced to reachability in hybrid automata.

HyLTL enables specifying complex properties beyond safety.

Existing tools can be used for verification via translation to hybrid automata.

Abstract

The model-checking problem for hybrid systems is a well known challenge in the scientific community. Most of the existing approaches and tools are limited to safety properties only, or operates by transforming the hybrid system to be verified into a discrete one, thus loosing information on the continuous dynamics of the system. In this paper we present a logic for specifying complex properties of hybrid systems called HyLTL, and we show how it is possible to solve the model checking problem by translating the formula into an equivalent hybrid automaton. In this way the problem is reduced to a reachability problem on hybrid automata that can be solved by using existing tools.