Towards Counterexample-Guided Computation of Validated Stability Certificates for Hybrid Systems

Eike Möhlmann and Oliver E. Theel
Proceedings of the 2nd Congreso Nacional de Ingenieria Informatica / Aplicaciones Informaticas y de Sistemas de Informacion, CoNaIISI 2014
We propose a method to obtain trustable Lyapunov-based certificates of stability for hybrid systems. A hybrid system is a system exhibiting discrete-time as well as continuous-time behaviors, e.g. embedded systems within a physical environment. Stability is a property which ensures that a system starting in any possible state will reach a desired state and remain there. Such systems are particularly useful when a certain autonomous operation is required, e.g. keeping a certain temperature or speed of a chemical reaction or steering a vehicle over a predefined track. Stable hybrid systems are extremely valuable because if an error disturbs their normal operation, they automatically "steer back" to normal operation. Stability can be certified by finding a so-called Lyapunov function. The search for this kind of functions usually involves solving systems of constraints. The state-of-the-art in Lyapunov-based stability verification is to use numerical methods to solve systems of inequalities, which if solvable indicate stability. We propose to use Satisfiability-Modulo-Theory (SMT) methods to (a) validate the results of a numerical solver and (b) use counterexamples to guide the numerical solver towards a valid solution.
Red de Carreras de Ingenieria Informatica / Sistemas de Information (RIISIC)
Marcelo M. Marciszack and Roberto M. Munoz and Mario A. Groppo