This paper provides a comprehensive review of formal controller synthesis techniques for safety-critical autonomous systems. It categorizes the formal control synthesis problem based on diverse system models (deterministic, non-deterministic, and stochastic) and various formal safety-critical specifications (logical, real-time, and real-valued domains). The review covers fundamental techniques, including abstraction-based approaches and abstraction-free methods, and explores the integration of data-driven synthesis approaches. The paper also discusses formal techniques tailored for multi-agent systems, addressing scalability challenges in large-scale systems. Finally, it highlights recent trends and research challenges in this area. - **Formal Methods**: Mathematically rigorous techniques for automated reasoning in complex dynamic systems. - **Safety-Critical Systems**: Systems where any malfunction can lead to significant catastrophes. - **Hybrid Dynamic Systems**: Systems with continuous dynamics and embedded control logics. - **Formal Control Synthesis**: Techniques to ensure provably correct control laws. - **Abstraction-Based Formal Control Synthesis**: Techniques for symbolic system models, including path planning, reactive control synthesis, and probabilistic synthesis. - **Abstraction-Free Formal Control Synthesis**: Techniques for continuous dynamic systems, such as optimization-based synthesis, Model Predictive Control, Control Barrier Functions, and sampling-based approaches. - **Data-Driven Formal Control Synthesis**: Approaches for synthesizing controllers from data, including formal abstractions, safe controller synthesis, and reinforcement learning. - **Deterministic Systems**: Open-loop planning problems. - **Non-Deterministic Systems**: Reactive control synthesis. - **Stochastic Systems**: Probabilistic synthesis with formal guarantees. - **Multi-Agent Systems**: Scalability challenges and tailored techniques. - **Recent Trends**: Data-driven methods, reinforcement learning, and scenario approaches. - **Research Challenges**: Ensuring scalability, handling complex specifications, and integrating with real-world systems.This paper provides a comprehensive review of formal controller synthesis techniques for safety-critical autonomous systems. It categorizes the formal control synthesis problem based on diverse system models (deterministic, non-deterministic, and stochastic) and various formal safety-critical specifications (logical, real-time, and real-valued domains). The review covers fundamental techniques, including abstraction-based approaches and abstraction-free methods, and explores the integration of data-driven synthesis approaches. The paper also discusses formal techniques tailored for multi-agent systems, addressing scalability challenges in large-scale systems. Finally, it highlights recent trends and research challenges in this area. - **Formal Methods**: Mathematically rigorous techniques for automated reasoning in complex dynamic systems. - **Safety-Critical Systems**: Systems where any malfunction can lead to significant catastrophes. - **Hybrid Dynamic Systems**: Systems with continuous dynamics and embedded control logics. - **Formal Control Synthesis**: Techniques to ensure provably correct control laws. - **Abstraction-Based Formal Control Synthesis**: Techniques for symbolic system models, including path planning, reactive control synthesis, and probabilistic synthesis. - **Abstraction-Free Formal Control Synthesis**: Techniques for continuous dynamic systems, such as optimization-based synthesis, Model Predictive Control, Control Barrier Functions, and sampling-based approaches. - **Data-Driven Formal Control Synthesis**: Approaches for synthesizing controllers from data, including formal abstractions, safe controller synthesis, and reinforcement learning. - **Deterministic Systems**: Open-loop planning problems. - **Non-Deterministic Systems**: Reactive control synthesis. - **Stochastic Systems**: Probabilistic synthesis with formal guarantees. - **Multi-Agent Systems**: Scalability challenges and tailored techniques. - **Recent Trends**: Data-driven methods, reinforcement learning, and scenario approaches. - **Research Challenges**: Ensuring scalability, handling complex specifications, and integrating with real-world systems.