Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance

随着自动驾驶技术的发展，高效的安全保障方法变得日益必要。监控和基于场景的测试等安全保障方法需要对驾驶场景进行形式化。本文采用信号时序逻辑（STL）作为逻辑形式化方法，对ISO标准34502中一个重要类别的关键场景进行了时序逻辑形式化。我们的形式化方法具有两个主要特征：1）采用ISO 34502的组合方法，对逻辑公式进行模块化组合，实现系统化和全面化的形式化；2）使用RSS距离来定义危险。由于RSS距离的使用，我们的形式化方法只需要很少的参数调整。我们进行了实验评估，通过其结果，我们讨论了我们的形式化方法的有效性以及其在选择某些参数值时的稳定性。

论文旨在开发一种基于信号时间逻辑（STL）的形式化方法，用于ISO标准34502中的关键场景的安全保证，以满足自动驾驶车辆的安全性需求。

论文使用信号时间逻辑（STL）作为逻辑形式，通过模块化组合逻辑公式来系统和全面地形式化驾驶场景，使用RSS距离来定义危险，避免了需要调整大量参数的问题。

论文的实验结果表明，该形式化方法的有效性和稳定性，作者还讨论了一些参数值的选择对结果的影响。实验使用了ISO 34502中的关键场景，作者还提供了开源代码。

近期的相关研究包括：'A Formal Framework for Verification of Autonomous Vehicle Control Systems'，'Scenario-Based Safety Validation of Autonomous Vehicles'，'A Survey of Motion Planning and Control Techniques for Self-Driving Urban Vehicles'等。