# Formal Synthesis of Controllers for Safety-Critical Autonomous Systems: Developments and Challenges

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

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 Feb 2024.

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

- [Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings](https://mlsanity.com/paper/2403.10497/) (2024)
- [TalkWithMachines: Enhancing Human-Robot Interaction for Interpretable Industrial Robotics Through Large/Vision Language Models](https://mlsanity.com/paper/2412.15462/) (2024)
- [Verifiable Natural Language to Linear Temporal Logic Translation: A Benchmark Dataset and Evaluation Suite](https://mlsanity.com/paper/2507.00877/) (2025)
- [Formal Control for Uncertain Systems via Contract-Based Probabilistic Surrogates (Extended Version)](https://mlsanity.com/paper/2506.16971/) (2025)
- [ReasonSTL: Bridging Natural Language and Signal Temporal Logic via Tool-Augmented Process-Rewarded Learning](https://mlsanity.com/paper/2605.06483/) (2026)
- [RRT*former: Environment-Aware Sampling-Based Motion Planning using Transformer](https://mlsanity.com/paper/2511.15414/) (2025)
- [GinSign: Grounding Natural Language Into System Signatures for Temporal Logic Translation](https://mlsanity.com/paper/2512.16770/) (2025)
- [Kernel-Based Learning of Safety Barriers](https://mlsanity.com/paper/2601.12002/) (2026)
- [GraSP-STL: A Graph-Based Framework for Zero-Shot Signal Temporal Logic Planning via Offline Goal-Conditioned Reinforcement Learning](https://mlsanity.com/paper/2603.29533/) (2026)
- [Safety Certification is Classification](https://mlsanity.com/paper/2605.06087/) (2026)
- [Reward Machines for Signal Temporal Logic](https://mlsanity.com/paper/2608.13625/) (2026)
- [Feedback Makes Perfect: A Closed-Loop Framework for NL-to-STL Translation](https://mlsanity.com/paper/2609.33287/) (2026)

## Abstract (arXiv)

In recent years, formal methods have been extensively used in the design of autonomous systems. By employing mathematically rigorous techniques, formal methods can provide fully automated reasoning processes with provable safety guarantees for complex dynamic systems with intricate interactions between continuous dynamics and discrete logics. This paper provides a comprehensive review of formal controller synthesis techniques for safety-critical autonomous systems. Specifically, we categorize the formal control synthesis problem based on diverse system models, encompassing deterministic, non-deterministic, and stochastic, and various formal safety-critical specifications involving logic, real-time, and real-valued domains. The review covers fundamental formal control synthesis techniques, including abstraction-based approaches and abstraction-free methods. We explore the integration of data-driven synthesis approaches in formal control synthesis. Furthermore, we review formal techniques tailored for multi-agent systems (MAS), with a specific focus on various approaches to address the scalability challenges in large-scale systems. Finally, we discuss some recent trends and highlight research challenges in this area.