AVACS H4

AVACS H4

AVACS - Subproject H4: Automatic Verification of Hybrid System Stability

Start of the project 2004, end of the project 2016

Description of the

AVACS Logo Hybrid systems are control systems that can contain both continuous-time behaviour and discrete state jumps. They therefore represent a combination of classical controllers (continuous-time) and computer-aided controllers (discrete-time) and are therefore particularly relevant in practice. Hybrid models are used, for example, for modelling embedded systems, biological systems or industrial processes. Stability refers to the property that temporally limited disturbances of the system do not permanently influence the behaviour, but are independently compensated by the system. A stable control system is therefore inherently robust against unforeseen disturbances. Stability is a liveness property of a system and is therefore usually difficult to prove. We concentrate on the proof of so-called asymptotic stability. A control system is globally asymptotically stable if it ultimately settles to a rest point for every possible initial state in the absence of disturbances. This resting point can be regarded as the desirable state of the system. The consequence is robustness against temporary disturbances of the system: the system will always return to the vicinity of the resting point when the disturbance effects subside. The proof of such a property can be provided by means of Lyapunov functions. Such a function can be understood as a measure of the energy of the system. If it is ensured that the energy minimum lies at the rest point and that the energy level continuously decreases over time, this can be used to prove global asymptotic stability. The central problem here is that such a function must be found -- this is a non-trivial task. The problem of finding such a Lyapunov function can be transformed into an efficiently solvable optimisation problem whose optimal solution is the parameterisation of such a Lyapunov function. Our goal is to advance these computational methods so that they can be integrated into verification tools. For example, decomposition methods are used that break down a large, possibly not numerically robust optimisation problem into several more robust ones. This makes it possible to analyse more complex systems than would otherwise be possible. Furthermore, we deal with the extension of these methods to systems with probabilistic behaviour and time delays.

Persons

Publications

Bibtex file not available or has no entries.
(Changed: 24 Jun 2026)  Kurz-URL:Shortlink: https://uol.de/p37598en
Zum Seitananfang scrollen Scroll to the top of the page

This page contains automatically translated content.