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

arXiv: https://arxiv.org/abs/2506.16971 · HTML: https://mlsanity.com/paper/2506.16971/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 20 of its 50 references that are in the map.
- First posted on arXiv 20 Jun 2025.

## Builds on (most cited first, 20 of 20)

- [Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems](https://mlsanity.com/paper/2405.06624/) (2024)
- [Automated Verification and Synthesis of Stochastic Hybrid Systems: A Survey](https://mlsanity.com/paper/2101.07491/) (2021)
- [International Scientific Report on the Safety of Advanced AI (Interim Report)](https://mlsanity.com/paper/2412.05282/) (2024)
- [Closed-loop Analysis of Vision-based Autonomous Systems: A Case Study](https://mlsanity.com/paper/2302.04634/) (2023)
- [Formal Synthesis of Controllers for Safety-Critical Autonomous Systems: Developments and Challenges](https://mlsanity.com/paper/2402.13075/) (2024)
- [Probabilities Are Not Enough: Formal Controller Synthesis for Stochastic Dynamical Models with Epistemic Uncertainty](https://mlsanity.com/paper/2210.05989/) (2022)
- [Verification of general Markov decision processes by approximate similarity relations and policy refinement](https://mlsanity.com/paper/1605.09557/) (2016)
- [Bayesian Formal Synthesis of Unknown Systems via Robust Simulation Relations](https://mlsanity.com/paper/2304.07428/) (2023)
- [Using Formal Methods for Autonomous Systems: Five Recipes for Formal Verification](https://mlsanity.com/paper/2012.00856/) (2020)
- [Context-triggered Abstraction-based Control Design](https://mlsanity.com/paper/2305.03399/) (2023)
- [Assume-Guarantee Reinforcement Learning](https://mlsanity.com/paper/2312.09938/) (2023)
- [Stochastic MPC with robustness to bounded parametric uncertainty](https://mlsanity.com/paper/2205.10275/) (2022)
- [Data-driven abstractions via adaptive refinements and a Kantorovich metric [extended version]](https://mlsanity.com/paper/2303.17618/) (2023)
- [Compositional Synthesis via a Convex Parameterization of Assume-Guarantee Contracts](https://mlsanity.com/paper/2002.06494/) (2020)
- [Compositional Reinforcement Learning for Discrete-Time Stochastic Control Systems](https://mlsanity.com/paper/2208.03485/) (2022)
- [SymAware: A Software Development Framework for Trustworthy Multi-Agent Systems with Situational Awareness](https://mlsanity.com/paper/2409.14833/) (2024)
- [Similarity quantification for linear stochastic systems: A coupling compensator approach](https://mlsanity.com/paper/2007.09052/) (2020)
- [SySCoRe: Synthesis via Stochastic Coupling Relations](https://mlsanity.com/paper/2302.12294/) (2023)
- [Verifying the Unknown: Correct-by-Design Control Synthesis for Networks of Stochastic Uncertain Systems](https://mlsanity.com/paper/2309.01276/) (2023)
- [Unraveling tensor structures in correct-by-design controller synthesis](https://mlsanity.com/paper/2503.24085/) (2025)

## Built on by (most cited first, 1 of 1)

- [Verification of Unknown Dynamical Systems via Autoencoder Latent Space](https://mlsanity.com/paper/2512.13593/) (2025)

## Abstract (arXiv)

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.