Stabhyli
Subproject |
H4 |
Categories |
Model checker / solver for hybrid systems |
Overview |
Stabhyli automatically proves a hybrid system stable. To do so, it takes a hybrid automaton as its input and constructs linear matrix inequality constraint systems based on the sums-of-squares decomposition. A solution to such a constraint system proves the hybrid system stable by employing Lyapunov functions that imply that the hybrid system's abstract energy decreases while the system evolves. As these constraint systems usually become very large the automaton's graph structure is exploited to decompose the hybrid system into small subcomponents. Stabhyli then solves the smaller constraint systems for each subcomponent successively. After solving the individual constraint systems the solutions (i.e., Lyapunov function) are re-composed in order to derive a global (piecewise) Lyapunov function that is valid for the whole automaton. Another benefit besides the need to solve only small constraint systems is that if the compositions fails, Stabhyli is able to give feedback on the critical part of the automaton, allowing for targeted redesign of the hybrid automaton. A detailed description of the decomposition technique is given in Decompositional Construction of Lyapunov Functions for Hybrid Systems (HSCC'09) by Jens Oehlerking and Oliver Theel. Currently a novel specialized input language specialized for modeling hybrid automata is used, and an automatic translation from HLang is planned. The input language allows the user to model hybrid systems using convex differential inclusions and (non-)deterministic or probabilistic state jumps using guards and updates on the continuous variables. |
Publications |
--- |
Adaptive Cruise Control Automaton |
|
Download |
Click here for binary & manual. |
Manual |
(see above) |
Status |
Prototype |