Computer-assisted proofs for Lyapunov stability via Sums of Squares certificates and Constructive Analysis
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2020
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866929445265211392 |
|---|---|
| author | Devadze, Grigory Magron, Victor Streif, Stefan |
| author_facet | Devadze, Grigory Magron, Victor Streif, Stefan |
| contents | We provide a computer-assisted approach to ensure that a given continuous or discrete-time polynomial system is (asymptotically) stable. Our framework relies on constructive analysis together with formally certified sums of squares Lyapunov functions. The crucial steps are formalized within of the proof assistant Minlog. We illustrate our approach with various examples issued from the control system literature. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2006_09884 |
| institution | arXiv |
| publishDate | 2020 |
| record_format | arxiv |
| spellingShingle | Computer-assisted proofs for Lyapunov stability via Sums of Squares certificates and Constructive Analysis Devadze, Grigory Magron, Victor Streif, Stefan Optimization and Control Logic in Computer Science We provide a computer-assisted approach to ensure that a given continuous or discrete-time polynomial system is (asymptotically) stable. Our framework relies on constructive analysis together with formally certified sums of squares Lyapunov functions. The crucial steps are formalized within of the proof assistant Minlog. We illustrate our approach with various examples issued from the control system literature. |
| title | Computer-assisted proofs for Lyapunov stability via Sums of Squares certificates and Constructive Analysis |
| topic | Optimization and Control Logic in Computer Science |
| url | https://arxiv.org/abs/2006.09884 |