Formal Methods for Control Synthesis of Autonomous Systems

Abstract

This talk provides an overview of practical applications of formal methods in the design of autonomous systems that are subject to complex rules. First, I will discuss the key assumptions and guarantees of different controller synthesis techniques for systems that are subject to temporal logic specifications, including closed system synthesis, probabilistic synthesis, and reactive synthesis. The second part of the talk focuses on self-driving cars that are subject to potentially conflicting rules, i.e., there are situations where the rules cannot be simultaneously satisfied. In order to handle such situations, I will introduce the concept of prioritized safety specifications and a class of temporal logic formulas that is sufficiently expressive to describe many traffic rules. Then, I will present an efficient, incremental sampling-based algorithm to compute a trajectory that minimizes the amount of rule violation. By avoiding the conversion of specifications into finite automata, the algorithm allows temporal logic specifications to be handled with the same computational complexity as traditional motion planning algorithms such as RRT* and RRG. Finally, I will wrap up the talk with a key bottleneck that prevents formal methods from realizing their full potential in the autonomous system domain—the (un)availability of formal specifications, which is a common, fundamental assumption all the temporal logic synthesis techniques rely on. I will discuss our early effort to partially address this problem and the remaining challenges.