Verifying the Unknown: Correct-by-Design Control Synthesis for Networks of Stochastic Uncertain Systems

TL;DR

This paper introduces a novel method for synthesizing correct-by-design controllers for networks of uncertain, stochastic, nonlinear systems using data-driven abstractions, addressing limitations of Gaussian assumptions and model availability.

Contribution

It extends abstraction-based control synthesis to networked uncertain systems with data-driven models and Gaussian mixture approximations, enabling formal control design under complex stochastic behaviors.

Findings

Successfully applied to a nonlinear package delivery case study.

Demonstrated control synthesis for a platoon of cars.

Quantified stochastic coupling effects in the control design.

Abstract

In this paper, we present an approach for designing correct-by-design controllers for cyber-physical systems composed of multiple dynamically interconnected uncertain systems. We consider networked discrete-time uncertain nonlinear systems with additive stochastic noise and model parametric uncertainty. Such settings arise when multiple systems interact in an uncertain environment and only observational data is available. We address two limitations of existing approaches for formal synthesis of controllers for networks of uncertain systems satisfying complex temporal specifications. Firstly, whilst existing approaches rely on the stochasticity to be Gaussian, the heterogeneous nature of composed systems typically yields a more complex stochastic behavior. Secondly, exact models of the systems involved are generally not available or difficult to acquire. To address these challenges, we show how abstraction-based control synthesis for uncertain systems based on sub-probability couplings can be extended to networked systems. We design controllers based on parameter uncertainty sets identified from observational data and approximate possibly arbitrary noise distributions using Gaussian mixture models whilst quantifying the incurred stochastic coupling. Finally, we demonstrate the effectiveness of our approach on a nonlinear package delivery case study with a complex specification, and a platoon of cars.