# Guarantees for Real Robotic Systems: Unifying Formal Controller Synthesis and Reachset-Conformant Identification

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 2 Mar 2021.

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

- [From Demonstrations to Safe Deployment: Path-Consistent Safety Filtering for Diffusion Policies](https://mlsanity.com/paper/2511.06385/) (2025)
- [CommonPower: A Framework for Safe Data-Driven Smart Grid Control](https://mlsanity.com/paper/2406.03231/) (2024)
- [Zono-Conformal Prediction: Zonotope-Based Uncertainty Quantification for Regression and Classification Tasks](https://mlsanity.com/paper/2508.11025/) (2025)
- [Leveraging Analytic Gradients in Provably Safe Reinforcement Learning](https://mlsanity.com/paper/2506.01665/) (2025)
- [Multi-Variable Conformal Prediction: Optimizing Prediction Sets without Data Splitting](https://mlsanity.com/paper/2605.12341/) (2026)

## Abstract (arXiv)

Robots are used increasingly often in safety-critical scenarios, such as robotic surgery or human-robot interaction. To ensure stringent performance criteria, formal controller synthesis is a promising direction to guarantee that robots behave as desired. However, formally ensured properties only transfer to the real robot when the model is appropriate. We address this problem by combining the identification of a reachset-conformant model with controller synthesis. Since the reachset-conformant model contains all the measured behaviors of the real robot, the safety properties of the model transfer to the real robot. The transferability is demonstrated by experiments on a real robot, for which we synthesize tracking controllers.