Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Xiang Yin, Bingzhao Gao, Xiao Yu

TL;DR

Safety-critical autonomous systems require automated, correct-by-construction controllers with formal guarantees framed as $\Sigma_C \models \varphi$. The paper surveys a broad taxonomy of formal control synthesis methods across deterministic, non-deterministic, and probabilistic models and across LTL/MTL/STL/CTL$^*$ specifications, highlighting both symbolic-abstraction and abstraction-free approaches. It covers data-driven and MAS extensions, including robustness, security, and AI-enabled directions, and discusses scalability strategies such as incremental product construction, MPC, CBFs, and compositional synthesis. The work outlines open challenges and future directions at the interface of formal guarantees and AI-enabled autonomy.

Abstract

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.

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

TL;DR

Safety-critical autonomous systems require automated, correct-by-construction controllers with formal guarantees framed as . The paper surveys a broad taxonomy of formal control synthesis methods across deterministic, non-deterministic, and probabilistic models and across LTL/MTL/STL/CTL specifications, highlighting both symbolic-abstraction and abstraction-free approaches. It covers data-driven and MAS extensions, including robustness, security, and AI-enabled directions, and discusses scalability strategies such as incremental product construction, MPC, CBFs, and compositional synthesis. The work outlines open challenges and future directions at the interface of formal guarantees and AI-enabled autonomy.

Abstract

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.
Paper Structure (31 sections, 1 figure, 2 tables)

This paper contains 31 sections, 1 figure, 2 tables.

Table of Contents

  1. Introduction
  2. Formal Control Synthesis Problems
  3. Formal System Models
  4. Formal Specification Languages
  5. Formal Control Synthesis Problems
  6. Abstraction-Based Formal Control Synthesis
  7. Construct Symbolic Models via Formal Abstractions
  8. Methods for Path Planning
  9. Methods for Reactive Control Synthesis
  10. Methods for Probabilistic Control Synthesis
  11. Abstraction-Free Formal Control Synthesis
  12. Synthesis via Optimizations
  13. Synthesis via Model Predictive Control
  14. Synthesis via Control Barrier Functions
  15. Synthesis via Sampling-Based Approaches
  16. ...and 16 more sections

Figures (1)

  • Figure 1: Organization of the paper.