# Feedback Refinement Relations for the Synthesis of Symbolic Controllers

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 12 Mar 2015.

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

- [Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions](https://mlsanity.com/paper/2301.01526/) (2023)
- [Decision-Making Under Uncertainty: Beyond Probabilities](https://mlsanity.com/paper/2303.05848/) (2023)
- [Correct-by-construction reach-avoid control of partially observable linear stochastic systems](https://mlsanity.com/paper/2103.02398/) (2021)
- [Neural Abstraction-Based Controller Synthesis and Deployment](https://mlsanity.com/paper/2307.03783/) (2023)
- [Efficient Dynamic Shielding for Parametric Safety Specifications](https://mlsanity.com/paper/2505.22104/) (2025)
- [Reversible Simplex Supervision with Post-Action Debt Accounting for Goal-Reaching RL](https://mlsanity.com/paper/2601.19499/) (2026)

## Abstract (arXiv)

We present an abstraction and refinement methodology for the automated controller synthesis to enforce general predefined specifications. The designed controllers require quantized (or symbolic) state information only and can be interfaced with the system via a static quantizer. Both features are particularly important with regard to any practical implementation of the designed controllers and, as we prove, are characterized by the existence of a feedback refinement relation between plant and abstraction. Feedback refinement relations are a novel concept introduced in this paper. Our work builds on a general notion of system with set-valued dynamics and possibly non-deterministic quantizers to permit the synthesis of controllers that robustly, and provably, enforce the specification in the presence of various types of uncertainties and disturbances. We identify a class of abstractions that is canonical in a well-defined sense, and provide a method to efficiently compute canonical abstractions. We demonstrate the practicality of our approach on two examples.