arXiv:2504.03272v1 交叉类型 摘要：本文提出了形式模型和形式安全证明，用于差分动态逻辑（dL）中的ABZ'25案例研究。该案例考虑了一辆自动驾驶汽车在高速公路上行驶，避免与相邻车辆发生碰撞。通过使用KeYmaera X的dL实现，我们在无限时间范围内证明了没有碰撞，从而确保了安全性不受行程长度的影响。这些安全保证适用于时间变化的反应时间和制动力。我们的dL模型考虑了单车道场景，包括前方或后方的车辆。我们证明了dL及其工具为运行时监控、防护和神经网络验证提供了一个严谨的基础。这样做揭示了ABZ'25研究中提供的规范和仿真环境highway-env之间的不一致之处。我们试图修正这些差异，并发现了许多反例，这些反例也表明提供的强化学习环境存在一些问题。