Formally Verified Neural Lyapunov Function for Incremental Input-to-State Stability of Unknown Systems
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909453581811712 |
|---|---|
| author | Basu, Ahan Dey, Bhabani Shankar Jagtap, Pushpak |
| author_facet | Basu, Ahan Dey, Bhabani Shankar Jagtap, Pushpak |
| contents | This work presents an approach to synthesize a Lyapunov-like function to ensure incrementally input-to-state stability ($δ$-ISS) property for an unknown discrete-time system. To deal with challenges posed by unknown system dynamics, we parameterize the Lyapunov-like function as a neural network, which we train using the data samples collected from the unknown system along with appropriately designed loss functions. We propose a validity condition to test the obtained function and incorporate it into the training framework to ensure provable correctness at the end of the training. Finally, the usefulness of the proposed technique is proved using two case studies: a scalar non-linear dynamical system and a permanent magnet DC motor. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_05778 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Formally Verified Neural Lyapunov Function for Incremental Input-to-State Stability of Unknown Systems Basu, Ahan Dey, Bhabani Shankar Jagtap, Pushpak Systems and Control This work presents an approach to synthesize a Lyapunov-like function to ensure incrementally input-to-state stability ($δ$-ISS) property for an unknown discrete-time system. To deal with challenges posed by unknown system dynamics, we parameterize the Lyapunov-like function as a neural network, which we train using the data samples collected from the unknown system along with appropriately designed loss functions. We propose a validity condition to test the obtained function and incorporate it into the training framework to ensure provable correctness at the end of the training. Finally, the usefulness of the proposed technique is proved using two case studies: a scalar non-linear dynamical system and a permanent magnet DC motor. |
| title | Formally Verified Neural Lyapunov Function for Incremental Input-to-State Stability of Unknown Systems |
| topic | Systems and Control |
| url | https://arxiv.org/abs/2501.05778 |