@inproceedingsconf/CoNaIISI/MohlmannT14,
Author = {Eike MÃ¶hlmann and Oliver E. Theel},
Title = {Towards Counterexample-Guided Computation of Validated Stability Certificates for Hybrid Systems},
Year = {2014},
Editor = {Marcelo M. Marciszack and Roberto M. Munoz and Mario A. Groppo},
Publisher = {Red de Carreras de Ingenieria Informatica / Sistemas de Information (RIISIC)},
Edition = {2},
Booktitle = {Proceedings of the 2nd Congreso Nacional de Ingenieria Informatica / Aplicaciones Informaticas y de Sistemas de Informacion, CoNaIISI 2014},
Url = {http://www.informatik.uni-oldenburg.de/~eikemoe/pubs/CoNaIISI_123.pdf},
type = {inproceedings},
note = {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 },
Abstract = {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.}
@COMMENTBibtex file generated on