Eintrag in der Universitätsbibliographie der TU Chemnitz
Volltext zugänglich unter
URN: urn:nbn:de:bsz:ch1-qucosa2-973437
Devadze, Grigory
Streif, Stefan ; Osinenko, Pavel (Gutachter)
Constructive analysis and computer-certified formal proofs for selected control-theoretical aspects
Kurzfassung in englisch
Nowadays, computers are indispensable devices in the daily work of scientists. Specifically, control engineers use the computers in the design, evaluation, simulation and optimization of complex control systems of different kind. Notably, the advances in numerical methods and computer hardware significantly impacted the application of the control theory on a wide range of real-world problems. It is well-known within the computer science community that computers are capable not only to work with numerical problems, but are also general information processing devices. This means that the computation can be applied to a wide range of different non-numeric data types: strings, lists, graphs, logical premises, computer programs themselves and even mathematical statement and their proofs. In context of the mathematical proofs, this phenomenon is also known as the so-called proofs-as-programs paradigm - a direct correspondence between computer programs and mathematical proofs. The idea is pretty simple: by the appropriate encoding of the mathematical statements, axioms and assumptions, derive a finite sequence of steps such that this sequence gets accepted by a certain computational device. The paradigm can be used for conceptional correctness, software verification and certification. This are undoubtedly desirable properties of any controller and/or controlled real-world system. Unfortunately, the classical model of the mathematics most commonly used for this purpose is not well-suitable, especially when dealing with the real numbers and continuous quantities, several issues regarding undecidability, non-computability and uncertainty arise. In contrast, this present work addresses the reasoning within the constructive analysis, which is a model of mathematics which is very close to computational devices and is valid within the framework of classical mathematics. This theoretical framework is applied to selected control-theoretical aspects, such as asymptotical stability of dynamical systems in sense of Lyapunov, existence of the solutions of ordinary differential equations, sliding-mode control and controller's verification. The work is motivated by various examples of different sources of the so-called computational uncertainty, i.e. a discrepancy between theoretical results and their computer realization, which might arise in the control theoretical applications. It demonstrates the principle possibility of deriving formal and computer-assisted proofs for the control theoretical purposes and thus contributing towards the so-called algorithmic control theory. The application of the derived theorems were demonstrated on several examples from control theory.
| Universität: | Technische Universität Chemnitz | |
| Institut: | Professur Regelungstechnik und Systemdynamik | |
| Fakultät: | Fakultät für Elektrotechnik und Informationstechnik | |
| Dokumentart: | Dissertation | |
| Betreuer: | Streif, Stefan | |
| DOI: | doi:10.60687/2025-0112 | |
| SWD-Schlagwörter: | Konstruktive Mathematik , Regelungstechnik | |
| Freie Schlagwörter (Englisch): | Constructive analysis , formal verification , control theory , computational uncertainty | |
| DDC-Sachgruppe: | 511.36, 629.8 | |
| Sprache: | englisch | |
| Tag der mündlichen Prüfung | 16.04.2025 |
