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

TL;DR

This paper introduces a scalable, abstraction-based method for formal control of uncertain stochastic systems using contract-based probabilistic surrogates, enabling effective decision-making with complex nonlinear interactions and infinite-horizon guarantees.

Contribution

It presents a novel approach that improves scalability of probabilistic simulation relations by avoiding direct error bound computations, facilitating control of high-dimensional nonlinear systems.

Findings

Enhanced scalability demonstrated on a high-dimensional vehicle intersection case study

Effective handling of complex nonlinear agent-environment interactions

Trade-off between conservatism and scalability validated

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.