基于时序自动机形式化建模与验证的数字公路法规
计算机科学中的逻辑
2022-09-29 v1 形式语言与自动机理论
软件工程
摘要
设计安全、可靠且可信的自动驾驶车辆（AVs）所面临的挑战之一，是确保 AVs 遵守交通规则。为此，AVs 需要能够理解并推理交通规则。在先前工作中，我们引入了空间交通逻辑 USL-TR，以实现交通规则无歧义、机器可读的形式化。这仅是迈向可验证遵守交通规则的自主交通智能体的第一步。在本研究预览中，我们聚焦于两个进一步步骤：a) 直接从交通规则提取行为图；b) 将行为图转换为在守卫与不变式中使用 USL-TR 公式的时序自动机。由此，我们获得了交通规则的形式化表示，并可迈向建立数字公路法规。我们简要展望了进一步步骤，包括向时序自动机添加环境与智能体模型，最终使用若干形式化验证工具实现并验证这些交通规则模型。
引用
@article{arxiv.2209.14036,
title = {Towards a Digital Highway Code using Formal Modelling and Verification of Timed Automata},
author = {Gleifer Vaz Alves and Maike Schwammberger},
journal= {arXiv preprint arXiv:2209.14036},
year = {2022}
}
备注
In Proceedings FMAS2022 ASYDE2022, arXiv:2209.13181