Formally Verified Neural Network Controllers for Incremental Input-to-State Stability of Unknown Discrete-Time Systems

This work aims to synthesize a controller that ensures that an unknown discrete-time system is incrementally input-to-state stable ($\delta$-ISS). In this work, we introduce the notion of $\delta$-ISS control Lyapunov function ($\delta$-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 $\delta$-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 $\delta$-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.