Safe Autonomy Under Perception Uncertainty Using Chance-Constrained Temporal Logic

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 t...

Full description

Saved in:
Bibliographic Details
Published in:Journal of automated reasoning 2018, Vol.60 (1), p.43-62
Main Authors: Jha, Susmit, Raman, Vasumathi, Sadigh, Dorsa, Seshia, Sanjit A.
Format: Article
Language:English
Subjects:
Artificial Intelligence
Autonomous vehicles
Autonomy
Computer Science
Constraints
Machine learning
Mathematical Logic and Formal Languages
Mathematical Logic and Foundations
Mixed integer
Optimal control
Perception
Specifications
Statistical analysis
Symbolic and Algebraic Manipulation
Synthesis
Temporal logic
Uncertainty
Vehicles
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0168-7433
1573-0670
DOI:10.1007/s10817-017-9413-9