Correct-by-Design Control of Parametric Stochastic Systems

TL;DR

This paper introduces new methods for designing controllers that are correct by construction for stochastic systems with parametric uncertainties, enabling formal safety guarantees for complex systems.

Contribution

It develops novel simulation relations based on coupling uncertainties, allowing for correct-by-design control refinement across parameterized models.

Findings

Established theoretical relations with closeness guarantees for linear and nonlinear systems.

Demonstrated methods on Van der Pol Oscillator and linear models.

Provided the first simulation relations for parametric stochastic systems.

Abstract

This paper addresses the problem of computing controllers that are correct by design for safety-critical systems and can provably satisfy (complex) functional requirements. We develop new methods for models of systems subject to both stochastic and parametric uncertainties. We provide for the first time novel simulation relations for enabling correct-by-design control refinement, that are founded on coupling uncertainties of stochastic systems via sub-probability measures. Such new relations are essential for constructing abstract models that are related to not only one model but to a set of parameterized models. We provide theoretical results for establishing this new class of relations and the associated closeness guarantees for both linear and nonlinear parametric systems with additive Gaussian uncertainty. The results are demonstrated on a linear model and the nonlinear model of the Van der Pol Oscillator.