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.

翻译：近年来，形式化方法已被广泛应用于自主系统设计。通过采用数学上严格的技术，形式化方法能够为连续动态与离散逻辑之间存在复杂交互的复杂动态系统提供具备可证明安全保证的全自动推理过程。本文对面向安全关键自主系统的形式化控制器综合技术进行了全面综述。具体而言，我们根据不同的系统模型（涵盖确定性、非确定性及随机系统）以及涉及逻辑、实时和实值域的各种形式化安全关键规范，对形式化控制综合问题进行了分类。综述涵盖了基础的形式化控制综合技术，包括基于抽象的方法和无抽象方法。我们探讨了数据驱动综合方法在形式化控制综合中的融合应用。此外，我们回顾了针对多智能体系统（MAS）的形式化技术，特别关注应对大规模系统可扩展性挑战的多种方法。最后，我们讨论了该领域的最新趋势，并重点阐述了研究挑战。