利用UPPAAL将活性引入多车道空间逻辑变道控制器
计算机科学中的逻辑
2018-04-13 v1 系统与控制
摘要
借助多车道空间逻辑(MLSL)提出了一种对自主交通机动进行形式化推理并证明安全性的强有力方法。基于MLSL构建了扩展时间自动机控制器,以在高速公路上执行安全变道机动。然而,该方法仅有少量实现与验证结果。因此我们强化MLSL方法,在UPPAAL中实现其变道控制器并确认变道协议的安全性。我们还检测到原控制器的不活跃行为,从而对其扩展并最终验证新变道控制器的活性。
引用
@article{arxiv.1804.04346,
title = {Introducing Liveness into Multi-lane Spatial Logic lane change controllers using UPPAAL},
author = {Maike Schwammberger},
journal= {arXiv preprint arXiv:1804.04346},
year = {2018}
}
备注
In Proceedings SCAV 2018, arXiv:1804.03406