基于时序逻辑对微观交通参数进行形式化与监控

智能城市正通过技术融合变革交通基础设施。然而，确保各类交通系统组件按预期且安全地运行是一大挑战。在本工作中，我们提出使用形式化方法作为指定和推理交通网络复杂属性的手段。形式化方法提供了一种灵活的工具，通过捕捉不符合规范的行为、探索交通场景的各种可能状态并检测其中的不一致性，来定义交通网络的安全运行。因此，我们利用形式语言信号时序逻辑（Signal Temporal Logic）开发了基于规范的监控以分析交通网络。我们开发了识别安全相关行为的监控器，例如遵守限速和保持适当车距。该框架使用经过标定的微观仿真高速公路场景进行测试，并将离线基于规范的监控应用于个体车辆轨迹，以理解其是否违反或满足所定义的安全规范。输出的统计分析表明，我们的方法能够根据所定义规范区分违规与合规的车辆轨迹。交通管理中心可利用本工作研究交通流属性、识别潜在危险，并为交通监控系统自动化提供有价值的反馈。