Click here to join the Zoom Webinar
ABSTRACT
Formal methods play an increasingly important role in ensuring the correctness of autonomous systems. In this talk, I will first describe various controller synthesis techniques for systems that are subject to temporal logic specifications. The focus will be on the key assumptions and guarantees of these different techniques, including closed system synthesis, probabilistic synthesis, reactive synthesis, and minimum violation planning, especially in the context of autonomous vehicles. The second part of the talk will focus on 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. Finally, I will discuss our early effort to partially address this problem and the remaining challenges.