Automated Synthesis of Safe Autonomous Vehicle Control Under Perception Uncertainty

Susmit Jha and Vasumathi Raman. Automated Synthesis of Safe Autonomous Vehicle Control Under Perception Uncertainty. (On Chance Constrained Signal Temporal Logic) NASA Formal Methods (NFM), 2016


Final NFM16 Version at ACM Digital Library
Accepted for publication at Journal of Automated Reasoning  


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.


 author = {Jha, Susmit and Raman, Vasumathi},
 title = {Automated Synthesis of Safe Autonomous Vehicle Control Under Perception Uncertainty},
 booktitle = {Proceedings of the 8th International Symposium on NASA Formal Methods - Volume 9690},
 series = {NFM 2016},
 year = {2016},
 isbn = {978-3-319-40647-3},
 location = {Minneapolis, MN, USA},
 pages = {117--132},
 numpages = {16},
 url = {},
 doi = {10.1007/978-3-319-40648-0_10},
 acmid = {2963385},
 publisher = {Springer-Verlag New York, Inc.},
 address = {New York, NY, USA},