从规范到行为：语义状态空间中的机动验证
机器人学
2019-12-02 v2 计算机科学中的逻辑
摘要
为实现自动驾驶汽车在可预见的未来进入市场，其行为规划系统需要遵守与人类相同的规则。若无针对审批困境的恰当解决方案，产品责任便无法落实。本文中，我们定义了连续空间的语义抽象，并用线性时序逻辑（LTL）形式化了交通规则。语义状态空间中的序列代表了高层规划器可选择执行的机动。我们使用运行时验证将这些机动与形式化后的交通规则进行核对。通过采用标准模型检测器 NuSMV，我们展示了方法的有效性，并给出了机动验证的运行时属性。我们表明，高层行为可在语义状态空间中得到验证以满一组形式化规则，这可作为迈向预期功能安全的一步。
引用
@article{arxiv.1905.00708,
title = {From Specifications to Behavior: Maneuver Verification in a Semantic State Space},
author = {Klemens Esterle and Vincent Aravantinos and Alois Knoll},
journal= {arXiv preprint arXiv:1905.00708},
year = {2019}
}
备注
Published at IEEE Intelligent Vehicles Symposium (IV), 2019