The demand for autonomous systems in safety-critical domains has increased in recent years. As real-world systems grow in complexity, a key challenge is ensuring robust performance under uncertainty, which requires the synthesis of controllers that not only operate reliably in st
...
The demand for autonomous systems in safety-critical domains has increased in recent years. As real-world systems grow in complexity, a key challenge is ensuring robust performance under uncertainty, which requires the synthesis of controllers that not only operate reliably in stochastic environments but also support post-hoc validation and certification of safety. To this end, Stochastic Model Predictive Control (SMPC) is a control framework suitable for systems subjected to stochastic disturbances and model uncertainties. However, its practical application is limited by the intractability of exact uncertainty propagation of the state distribution (i.e. the prediction step), particularly for nonlinear dynamics, incentivising research to focus on approximation methods such as linearisation or Monte Carlo sampling. In this literature, however, the approximations do not provide guarantees of correctness. This work addresses this particular limitation by leveraging quantisation-based uncertainty propagation, where both the state and disturbance distributions are discretised with formal guarantees in the Wasserstein distance. We formulate a quantised SMPC algorithm for discrete-time nonlinear systems with Gaussian additive noise, subject to individual chance constraints. For safety certification of the obtained controller, we introduce a validation scheme based on Wasserstein ambiguity sets that estimate worst-case constraint violation probabilities. The proposed approach is evaluated in simulation on benchmark tasks under both open and closed-loop policies.