Formal Control for Uncertain Systems via Contract-Based Probabilistic Surrogates (Extended Version)
This work addresses scalability issues in formal control for uncertain systems, which is crucial for applications like autonomous vehicles, though it appears incremental in enhancing existing abstraction-based techniques.
The paper tackles the challenge of scalability in formal methods for uncertain systems by proposing an approach that eliminates the need to compute error bounds, using probabilistic simulation relations and surrogate models. It demonstrates improved scalability and applicability in a high-dimensional vehicle intersection case study, trading scalability for conservatism effectively.
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.