Formal Control for Uncertain Systems via Contract-Based Probabilistic Surrogates (Extended Version)

TL;DR

The paper tackles the scalability challenge of formal controller synthesis for uncertain CPS by introducing an assume–guarantee contract (AGC) framework that reasons about a complex environment ${\mathbf{E}}$ via a surrogate ${\mathbf{S}}$ under an adversarial disturbances ${\mathfrak{n}}$ and model uncertainty ${\theta}$. It extends stochastic simulation relations with behavioral inclusion (BI) and sub-simulation relations (SSRs) to handle nondeterministic adversaries, enabling controller synthesis for the interconnected system ${\mathbf{A}}\times{\mathbf{E}}$ through a reduced-order proxy ${\mathbf{A}}_{r}\times{\mathbf{S}}$. The main theoretical result (Theorem) shows how an $(\varepsilon,\delta)$-guarantee can be propagated from $({\mathbf{A}}_{r}\times{\mathbf{S}})$ to $({\mathbf{A}}\times{\mathbf{E}})$ via an appropriate relation, interface, and MOR compensator, thus avoiding direct high-dimensional error bound computation. The approach is demonstrated on a high-dimensional traffic intersection case, achieving a reduced 9D to 4D proxy with an abstraction error $(\varepsilon_3,\delta_3)=(0.2,14.96\%)$, yielding a robust satisfaction probability of $p=58\%$ in one scenario (real performance ≈ $67\%$) and $p=19\%$ in another (real ≈ $41\%$), highlighting scalability and conservatism trade-offs while validating the AGC methodology for uncertain, nonlinear stochastic systems.

Abstract

The requirement for identifying accurate system representations has not only been a challenge to fulfill, but it has compromised the scalability of formal methods, as the resulting models are often too complex for effective decision making with formal correctness and performance guarantees. Focusing on probabilistic simulation relations and surrogate models of stochastic systems, we propose an approach that significantly enhances the scalability and practical applicability of such simulation relations by eliminating the need to compute error bounds directly. As a result, we provide an abstraction-based technique that scales effectively to higher dimensions while addressing complex nonlinear agent-environment interactions with infinite-horizon temporal logic guarantees amidst uncertainty. Our approach trades scalability for conservatism favorably, as demonstrated on a complex high-dimensional vehicle intersection case study.

Figures (1)

• Figure 1: Design a robust controller ${\mathbf{{C}}}$ for an agent ${\mathbf{{A}}}$ based on finitely many surrogate models $\{{\mathbf{{S}}}_i\}_{i\in\mathcal{I}}$ and obtain formal guarantees for its performance (with respect to some specification $\psi$ and satisfaction probability $p_{\text{\normalfont{c}}}$) once deployed in the concrete environment ${\mathbf{{E}}}$. The model discrepancies arising from uncertainty and incomplete information are modeled via an uncertain parametrization $\theta\in\Theta$ and a nondeterministic adversary ${{\mathfrak{{n}}}}\in{{\mathfrak{{N}}}}$.