Automated detection and elimination of implicit equivalences in quantified non-linear inequality systems for stability verification of hybrid systems using Lyapunov theory
Automated detection and elimination of implicit equivalences in quantified non-linear inequality systems for stability verification of hybrid systems using Lyapunov theory
Automated detection and elimination of implicit equivalences in quantified non-linear inequality systems for stability verification of hybrid systems using Lyapunov theory
Bachelor thesis
completed in 2015 by Philipp Zschoche
Subject areas
- Hybrid Systems
- Lyapunov stability
- Automatic verification
- Numerical Optimisation
- Graph Theory
Background
Hybrid systems are dynamic systems that exhibit both discrete and continuous behaviour.
The stability verification of linear and non-linear hybrid systems is generally an undecidable problem. It is possible to verify the stability of a hybrid system using Lyapunov functions.
Stabhyli is a programme for automatic stability verification of non-linear hybrid systems using Lyapunov functions. When searching for suitable Lyapunov functions, a non-linear inequality system of conditions is created in which each condition corresponds to the following form:
f(0) = 0 ∧ ∀ x ∈ R : 0 ≤ f(x) where f is polynomial and R is a region of the hybrid system
Numerical problems can lead to incorrect solutions of these conditions. Small gaps are inserted to increase the robustness against numerical problems.
If an inequality system contains implicit equivalences, this robustness extension can lead to there no longer being a solution. Stability verification is no longer possible.
It is therefore particularly important to find and eliminate implicit equivalences.
Job description
In this bachelor thesis, the detection and elimination of implicit equivalences in relation to the stability verification of hybrid systems using Lyapunov functions will be investigated.
In particular, Stabhyli will be extended by an already described heuristic to detect implicit equivalences.
For the elimination, a backtracking algorithm will be developed and implemented that removes known implicit equivalences from the given system of equations and optimises them for problem solvers such as CSDP and SDPA.
Furthermore, it will be evaluated whether the developed method can be further refined, e.g., by adding a scoring function for the backtracking algorithm:
- With an evaluation function for the backtracking algorithm
- Searching again for implicit equivalences after an implicit equivalence has been eliminated.