UC Berkeley

Autonomous vehicles have found wide-ranging adoption in aerospace, terrestrial as well as marine use. These systems often operate in uncertain environments and in the presence of noisy sensors, and use machine learning and statistical sensor fusion algorithms to form an internal model of the world that is inherently probabilistic. Autonomous vehicles need to operate using this uncertain world-model, and hence, their correctness cannot be deterministically specified. Even once probabilistic correctness is specified, proving that an autonomous vehicle will operate correctly is a challenging problem. In this paper, we address these challenges by proposing a correct-by-synthesis approach to autonomous vehicle control. We propose a probabilistic extension of temporal logic, named Chance Constrained Temporal Logic (C2TL), that can be used to specify correctness requirements in presence of uncertainty. C2TL extends temporal logic by including chance constraints as predicates in the formula which allows modeling of perception uncertainty while retaining its ease of reasoning. We present a novel automated synthesis technique that compiles C2TL specification into mixed integer constraints, and uses second-order (quadratic) cone programming to synthesize optimal control of autonomous vehicles subject to the C2TL specification. We also present a risk distribution approach that enables synthesis of plans with lower cost without increasing the overall risk. We demonstrate the effectiveness of the proposed approach on a diverse set of illustrative examples.