In this paper, we present an automatable decompositional method for the computation of Lyapunov functions for hybrid systems
with complex discrete state spaces. We use graph-based reasoning to decompose hybrid automata into subgraphs, for which we
then solve semidefinite optimization problems to obtain local Lyapunov functions. These local computations are made in a way
that ensures that the family of local Lyapunov functions forms a global Lyapunov function, proving asymptotic stability of
the system. The main advantages over standard LMI methods are 1) improved numerical stability due to smaller optimization
problems, 2) the possibility of incremental construction of stable hybrid automata and 3) easier diagnosis of unstable parts
of the automaton in case no Lyapunov function can be found.
This work was partly supported by the German Research Foundation (DFG) as part of the Transregional Research Center “Automatic
Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS),
www.avacs.org
.