Stabhyli - A Tool for Automatic Stability Verification of Non-linear Hybrid Systems
Stabhyli is a tool that automatically proves stability (global asymptotic stability) of non-linear hybrid systems. The tool was created in the context of AVACS H4.
Hybrid systems are systems that exhibit discrete as well as continuous behavior. The stability property basically ensures that a system exposed to a faulty environment (e.g. suffering from disturbances) will be able to regain a "good" operation mode as long as errors occur not too frequently. Stabilizing hybrid systems are omnipresent, for instance in control applications where a discrete controller is controlling a time-continuous process such as a car's movement or a particular chemical reaction. Stabhyli automatically derives a certificate of stability for a given non-linear hybrid systems. Such certificates are obtained by Lyapunov theory combined with decomposition and composition techniques.
E. Möhlmann und O. E. Theel, "Stabhyli: A Tool for Automatic Stability Verification of Non-Linear Hybrid Systems" in Proc. Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'13, 2013.
@inproceedings{conf/hybrid/MohlmannT13,
author = {Eike M{\"o}hlmann and Oliver E. Theel},
title = {Stabhyli: {A} {T}ool for {A}utomatic {S}tability {V}erification of {N}on-{L}inear {H}ybrid {S}ystems},
booktitle = {Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'13},
year = {2013},
pages = {107-112},
url = {http://doi.acm.org/10.1145/2461328.2461347},
crossref = {DBLP:conf/hybrid/2013},
location = {Philadelphia, Pennsylvania, USA},
acmid = {2461347},
keywords = {LMIS, automatic verification, computer-aided design, hybrid systems, lyapunov theory, stability, sums-of-squares},
abstract = {We present Stabhyli, a tool that automatically proves stability of non-linear hybrid systems. Hybrid systems are systems that exhibit discrete as well as continuous behavior. The stability property basically ensures that a system exposed to a faulty environment (e.g. suffering from disturbances) will be able to regain a "good" operation mode as long as errors occur not too frequently. Stabilizing Hybrid systems are omnipresent, for instance in control applications where a discrete controller is controlling a time-continuous process such as a car's movement or a particular chemical reaction. We have implemented a tool to automatically derive a certificate of stability for non-linear hybrid systems. Certificates are obtained by Lyapunov theory combined with decomposition and composition techniques.},
editor = {Calin Belta and Franjo Ivancic},
publisher = {ACM},
isbn = {978-1-4503-1567-8},
}
E. Möhlmann und O. E. Theel, "Towards Automatic Detection of Implicit Equality Constraints in Stability Verification of Hybrid Systems" in Proc. Proceedings of the 1th Congreso Nacional de Ingeniería Informática / Aplicaciones Informáticas y de Sistemas de Información, CoNaIISI 2013, 2013.
@inproceedings{conf/CoNaIISI/MohlmannT13,
author = {Eike M{\"o}hlmann and Oliver E. Theel},
title = {{Towards Automatic Detection of Implicit Equality Constraints in Stability Verification of Hybrid Systems}},
booktitle = {Proceedings of the 1th Congreso Nacional de Ingeniería Inform{\'{a}}tica / Aplicaciones Inform{\'{a}}ticas y de Sistemas de Informaci{\'{o}}n, CoNaIISI 2013},
year = {2013},
url = {http://conaiisi.frc.utn.edu.ar/PDFsParaPublicar/1/schedConfs/1/104-504-1-DR.pdf},
location = {C{\'{o}}rdoba, C{\'{o}}rdoba, Argentina},
keywords = {Hybrid Systems; Automatic Verification; Stability; Lyapunov Theory; Optimization; Sums-of-Squares},
editor = {Marcelo M. Marciszack and Roberto M. Mu{\~{n}}oz and Mario A. Groppo},
publisher = {Red de Carreras de Ingenier{\'{i}}a Inform{\'{a}}tica / Sistemas de Informati{\'{o}}n (RIISIC)},
issn = {2346-9927},
abstract = {We present a powerful heuristic that detects implicit equality constraints that may occur in the specification of systems of constraints in order to find Lyapunov-based certificates of stability for hybrid systems. A hybrid system is a fusion of systems exhibiting discrete-time as well as continuous-time behavior, 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 where 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 after an error has disturbed their normal operation, they automatically \enquote{steer back} to normal operation. Stability can be certified by finding a so-called Lyapunov function. The search for this kind of function usually involves solving systems of inequality constraints. We have identified and implemented a heuristic that detects implicitly specified equality constraints and tries to resolve them by substitution.},
}
E. Möhlmann und O. E. Theel, "Towards Counterexample-Guided Computation of Validated Stability Certificates for Hybrid Systems" in Proc. Proceedings of the 2nd Congreso Nacional de Ingeniería Informática / Aplicaciones Informáticas y de Sistemas de Información, CoNaIISI 2014, 2014.
@inproceedings{conf/CoNaIISI/MohlmannT14,
author = {Eike M{\"o}hlmann and Oliver E. Theel},
title = {{Towards Counterexample-Guided Computation of Validated Stability Certificates for Hybrid Systems}},
year = {2014},
month = {November},
issn = {2346-9927},
editor = {Marcelo M. Marciszack and Roberto M. Mu{\~{n}}oz and Mario A. Groppo},
booktitle = {Proceedings of the 2nd Congreso Nacional de Ingeniería Inform{\'{a}}tica / Aplicaciones Inform{\'{a}}ticas y de Sistemas de Informaci{\'{o}}n, CoNaIISI 2014},
location = {San Luis, Argentina},
publisher = {Red de Carreras de Ingenier{\'{i}}a Inform{\'{a}}tica / Sistemas de Informati{\'{o}}n (RIISIC)},
volume = {2},
issn = {2346-9927},
url = {http://www.informatik.uni-oldenburg.de/~eikemoe/pubs/CoNaIISI_123.pdf},
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.},
