Formally Verified Neural Network Controllers for Incremental Input-to-State Stability of Unknown Discrete-Time Systems
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909870360363008 |
|---|---|
| author | Basu, Ahan Dey, Bhabani Shankar Jagtap, Pushpak |
| author_facet | Basu, Ahan Dey, Bhabani Shankar Jagtap, Pushpak |
| contents | This work aims to synthesize a controller that ensures that an unknown discrete-time system is incrementally input-to-state stable ($δ$-ISS). In this work, we introduce the notion of $δ$-ISS control Lyapunov function ($δ$-ISS-CLF), which, in conjunction with the controller, ensures that the closed-loop system is incrementally ISS. To address the unknown dynamics of the system, we parameterize the controller as well as the $δ$-ISS-CLF as neural networks and learn them by utilizing the sampled data from the state space of the unknown system. To formally verify the obtained $δ$-ISS-CLF, we develop a validity condition and incorporate the condition into the training framework to ensure a provable correctness guarantee at the end of the training process. Finally, the usefulness of the proposed approach is proved using multiple case studies - the first one is a scalar system with a non-affine non-polynomial structure, the second example is a one-link manipulator system, the third system is a nonlinear Moore-Grietzer model of the jet engine and the final one is a rotating rigid spacecraft model. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_04129 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Formally Verified Neural Network Controllers for Incremental Input-to-State Stability of Unknown Discrete-Time Systems Basu, Ahan Dey, Bhabani Shankar Jagtap, Pushpak Systems and Control This work aims to synthesize a controller that ensures that an unknown discrete-time system is incrementally input-to-state stable ($δ$-ISS). In this work, we introduce the notion of $δ$-ISS control Lyapunov function ($δ$-ISS-CLF), which, in conjunction with the controller, ensures that the closed-loop system is incrementally ISS. To address the unknown dynamics of the system, we parameterize the controller as well as the $δ$-ISS-CLF as neural networks and learn them by utilizing the sampled data from the state space of the unknown system. To formally verify the obtained $δ$-ISS-CLF, we develop a validity condition and incorporate the condition into the training framework to ensure a provable correctness guarantee at the end of the training process. Finally, the usefulness of the proposed approach is proved using multiple case studies - the first one is a scalar system with a non-affine non-polynomial structure, the second example is a one-link manipulator system, the third system is a nonlinear Moore-Grietzer model of the jet engine and the final one is a rotating rigid spacecraft model. |
| title | Formally Verified Neural Network Controllers for Incremental Input-to-State Stability of Unknown Discrete-Time Systems |
| topic | Systems and Control |
| url | https://arxiv.org/abs/2503.04129 |