Hybrid tools for hybrid systems – Proving stability and safety at once

Abstract

Industrial applications usually require safety and stability properties. The safety property guarantees that “something bad” never happens, and the stability property guarantees that “something good” eventually happens. The analyses of both properties are usually performed in isolation. In this work, we consider analyzing both properties by a single automatic approach for hybrid systems. We basically merge analyses of both properties to exploit the knowledge gained from the analysis of each of them in the analysis of the other. We show how both analyses can be divided into multiple steps and interlocked such that both benefit from each other. In fact, we compute single-mode Lyapunov functions, unroll the hybrid system’s automaton via repeated reachability queries, and, finally, compute a global Lyapunov function. Each reachability query is simplified by exploiting the knowledge gained from the single-mode Lyapunov functions. The final computation of the global Lyapunov function is simplified by a precise characterization of the reachable states and reuses the single-mode Lyapunov functions. We provide automated tools necessary to link the analyses and report on promising experiments we performed using our new prototype tool.