Automated Synthesis of Safe Autonomous Vehicle Control Under Perception Uncertainty

Automated Synthesis of Safe Autonomous Vehicle Control Under Perception Uncertainty
复制标题

感知不确定性下安全自主车辆控制的自动综合

DOI:
--
复制
发表时间:
2016
期刊:
NASA Formal Methods
影响因子:
--
通讯作者:
Vasumathi Raman
Vasumathi Raman
中科院分区:
--
文献类型:
--
作者:
Susmit Jha;Vasumathi Raman

文献摘要

参考文献

被引文献

相似文献

自动驾驶车辆在航空航天、陆地以及海洋应用中得到了广泛采用。这些系统通常在不确定的环境中运行,且传感器存在噪声,并使用机器学习和统计传感器融合算法来形成一个本质上具有概率性的世界内部模型。自动驾驶车辆需要使用这种不确定的世界模型来运行,因此,其正确性无法确定性地规定。即使规定了概率正确性,证明自动驾驶车辆将正确运行也是一个具有挑战性的问题。在本文中,我们通过提出一种综合即正确的自动驾驶车辆控制方法来应对这些挑战。我们提出了一种时序逻辑的概率扩展,名为机会约束时序逻辑(C2TL),它可用于在存在不确定性的情况下规定正确性要求。我们提出了一种新颖的自动综合技术,该技术将C2TL规范编译为混合整数约束,并使用二阶二次锥规划来根据C2TL规范综合自动驾驶车辆的最优控制。我们通过一系列多样化的示例展示了所提方法的有效性。
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. 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 demonstrate the effectiveness of the proposed approach on a diverse set of illustrative examples.
无人机系统的安全和认证
DOI: 10.1049/etr.2015.0009
发表时间: 2015
期刊: Engineering & Technology Reference
影响因子: --
作者:
Patchett C
通讯作者: Patchett C