Formal analysis tools for nonlinear model-predictive control : formal verification techniques for real-world MPC
Ramesh Krishnamurthy · 2025
Model Predictive Control (MPC) is a widely used strategy for controlling systems with constraints, offering the ability to optimize control actions over a finite horizon while anticipating future behavior. Its applicability spans domains such as robotics, autonomous driving, and process control. Yet in practice, engineers still face two long-standing obstacles in deploying nonlinear MPC on embedded and safety-critical systems: (i) the absence of formal correctness guarantees, and (ii) the unpredictability of worst-case execution time (WCET). These two aspects make it difficult to argue that nonlinear MPC will always produce the right decision within the available time, both of which are required for certification. This thesis addresses these challenges through an integrated approach that combines learning-based approximation, formal verification, and timing analysis. Rather than relying solely on controller approximation or exhaustive simulation, the proposed framework rests on the central idea that performance, correctness, and real-time execution must be addressed together in a unified manner. To mitigate the computational burden of solving MPC online, we present a learning-based surrogate control strategy that uses verified integration via Taylor models to improve the training of neural network approximators. By enhancing the DAgger framework with numerical methods, we generate informative training data that remains faithful to the original MPC policy, improving both efficiency and generalization. To assess correctness, we propose a regret-based competitive analysis technique that quantifies the deviation of learned policies from the MPC baseline. Using hybrid automata models and reachability tools such as Verisig and Flow*, we evaluate the closed-loop behavior of neural network surrogates and provide formal bounds on their performance. Finally, we develop a WCET analysis framework tailored to nonlinear MPC solvers. This includes a comparison of test-generation strategies—state-space partitioning, closed-loop simulation, and complexity certification—and the application of certified complexity bounds to active-set solvers. These contributions enable formal reasoning about solver runtime under varying inputs and workloads. The proposed methods are validated on three nonlinear control tasks: motion planning of a truck-trailer system, an inverted cart-pendulum, and a constrained bicycle model. Together, these contributions offer both a methodology and a set of tools that demonstrate how learning, verification, and timing analysis can be jointly leveraged to bring nonlinear MPC closer to certified deployment in real-time embedded systems.