Lyapunov abstractions for inevitability of hybrid systems

A set of states S is said to be inevitable for a hybrid automaton A if every behavior of A ultimately reaches S within bounded time. Inevitability captures various commonly occurring liveness properties. In this paper, we present an algorithm for verifying inevitability of Linear Hybrid Automata (LHA). The algorithm combines (a) Lyapunov function-based relational abstractions for the continuous dynamics with (b) automated construction of well-founded relations for the loops of the hybrid automaton. The algorithm is complete for automata that are symmetric with respect to the chosen Lyapunov functions. The algorithm is implemented in a prototype tool (LySHA) which is integrated with a Simulink/Stateflow frontend for modeling hybrid systems. The experimental results demonstrate the effectiveness of the methodology in verifying inevitability of hybrid automata with up to five continuous dimensions and forty locations.