Verifying the Unknown: Correct-by-Design Control Synthesis for Networks of Stochastic Uncertain Systems
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Learning Robust Policies for Uncertain Parametric Markov Decision Processes
Synthesising verifiably correct controllers for dynamical systems is crucial for safety-critical problems. To achieve this, it is important to account for uncertainty in a robust manner, while at the same time it is ofte…
Data-Driven Abstraction-Based Control Synthesis
This paper studies formal synthesis of controllers for continuous-space systems with unknown dynamics to satisfy requirements expressed as linear temporal logic formulas. Formal abstraction-based synthesis schemes rely o…
Correct-by-synthesis reinforcement learning with temporal logic constraints
We consider a problem on the synthesis of reactive controllers that optimize some a priori unknown performance criterion while interacting with an uncontrolled environment such that the system satisfies a given temporal …
Motion PlanningQ-Learningreinforcement-learningReinforcement Learning+1Bayesian Formal Synthesis of Unknown Systems via Robust Simulation Relations
This paper addresses the problem of data-driven computation of controllers that are correct by design for safety-critical systems and can provably satisfy (complex) functional requirements. With a focus on continuous-spa…
Ternary Logic Encodings of Temporal Behavior Trees with Application to Control Synthesis
Behavior Trees (BTs) provide designers an intuitive graphical interface to construct long-horizon plans for autonomous systems. To ensure their correctness and safety, rigorous formal models and verification techniques a…