Notes on Recent Achievements in Proving Stability using KeYmaeraX
KeYmaeraX is a Hoare-style theorem prover for hybrid systems. A hybrid system can be seen as an aggregation of both discrete and continuous variables, whose values can change abruptly or continuously, respectively. KeYmaeraX supports only variables having the primitive type bool or real. Due to the...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2021-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/1563 |
| _version_ | 1797877852315582464 |
|---|---|
| author | Thomas Baar Horst Schulte |
| author_facet | Thomas Baar Horst Schulte |
| author_sort | Thomas Baar |
| collection | DOAJ |
| description | KeYmaeraX is a Hoare-style theorem prover for hybrid systems. A hybrid system can be seen as an aggregation of both discrete and continuous variables, whose values can change abruptly or continuously, respectively. KeYmaeraX supports only variables having the primitive type bool or real. Due to the mixture of discrete and continuous system elements, one promising application area for KeYmaeraX are closed-loop control systems. A closed-loop control system consists of a plant and a controller. While the plant is basically an aggregation of continuous variables whose values change over time accordingly to physical laws, the controller can be seen as an algorithm formulated in a classical programming language. In this paper, we review some recent extensions of the proof calculus applied by KeYmaeraX that make formal proofs on the stability of dynamic systems more feasible. Based on an example, we first introduce to the topic and prove asymptotic stability of a given system in a hand-written mathematical style. This approach is then compared with a formal encoding of the problem and a formal proof established in KeYmaeraX. We also discuss open problems such as the formalization of asymptotic stability. |
| first_indexed | 2024-04-10T02:23:44Z |
| format | Article |
| id | doaj.art-11cd679b7a5c4381aa8592fd10259101 |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2024-04-10T02:23:44Z |
| publishDate | 2021-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-11cd679b7a5c4381aa8592fd102591012023-03-13T08:07:35ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172021-12-0128432633610.18255/1818-1015-2021-4-326-3361194Notes on Recent Achievements in Proving Stability using KeYmaeraXThomas Baar0Horst Schulte1Университет прикладных технических и экономических наук г. БерлинаУниверситет прикладных технических и экономических наук г. БерлинаKeYmaeraX is a Hoare-style theorem prover for hybrid systems. A hybrid system can be seen as an aggregation of both discrete and continuous variables, whose values can change abruptly or continuously, respectively. KeYmaeraX supports only variables having the primitive type bool or real. Due to the mixture of discrete and continuous system elements, one promising application area for KeYmaeraX are closed-loop control systems. A closed-loop control system consists of a plant and a controller. While the plant is basically an aggregation of continuous variables whose values change over time accordingly to physical laws, the controller can be seen as an algorithm formulated in a classical programming language. In this paper, we review some recent extensions of the proof calculus applied by KeYmaeraX that make formal proofs on the stability of dynamic systems more feasible. Based on an example, we first introduce to the topic and prove asymptotic stability of a given system in a hand-written mathematical style. This approach is then compared with a formal encoding of the problem and a formal proof established in KeYmaeraX. We also discuss open problems such as the formalization of asymptotic stability.https://www.mais-journal.ru/jour/article/view/1563киберфизическая систематеория управленияфункция ляпуноваимперативный язык программирования |
| spellingShingle | Thomas Baar Horst Schulte Notes on Recent Achievements in Proving Stability using KeYmaeraX Моделирование и анализ информационных систем киберфизическая система теория управления функция ляпунова императивный язык программирования |
| title | Notes on Recent Achievements in Proving Stability using KeYmaeraX |
| title_full | Notes on Recent Achievements in Proving Stability using KeYmaeraX |
| title_fullStr | Notes on Recent Achievements in Proving Stability using KeYmaeraX |
| title_full_unstemmed | Notes on Recent Achievements in Proving Stability using KeYmaeraX |
| title_short | Notes on Recent Achievements in Proving Stability using KeYmaeraX |
| title_sort | notes on recent achievements in proving stability using keymaerax |
| topic | киберфизическая система теория управления функция ляпунова императивный язык программирования |
| url | https://www.mais-journal.ru/jour/article/view/1563 |
| work_keys_str_mv | AT thomasbaar notesonrecentachievementsinprovingstabilityusingkeymaerax AT horstschulte notesonrecentachievementsinprovingstabilityusingkeymaerax |