扩展城市多车道空间逻辑以形式化道路交叉口规则

在自动驾驶车辆(AVs)的设计过程中,若干阶段应包含验证过程,以保证AV在道路上安全行驶。其中之一是确保AV遵守道路交通规则。为了在AV设计中纳入道路交通规则,需要对这些规则进行精确且无歧义的形式化。然而,直到最近这一点才被指出是AV设计中的一个问题,且仅有少数相关工作仅捕捉了规则的时间方面,忽略了空间方面。在此,我们扩展了空间交通逻辑——城市多车道空间逻辑(Urban Multi-lane Spatial Logic),以形式化英国道路交叉口规则的一个子集,其中同时捕捉了规则的时间与空间方面。我们的方法对城市道路交叉口具有一种抽象层次,可轻易促进整套道路交叉口规则的形式化,并且我们示例性地形式化了三条英国道路交叉口规则。一旦我们完成了整套规则的形式化,我们将针对道路交通规则对AV的行为进行建模、实现与形式化验证,从而能够建立面向AV的数字公路法规的指南。