基于区域的时间自动机验证：外推、模拟及下一步？

时间自动机由 Rajeev Alur 和 David Dill 于 90 年代初提出。在过去的几十年中，时间自动机已成为实时系统验证的事实标准模型。时间自动机的算法基于使用区域作为符号表示来遍历其状态空间。由于状态空间是无限的，终止依赖于产生可达状态有限表示的有限抽象。获得有限抽象的第一个解决方案基于区域的外推，并已在工业级工具 Uppaal 中实现。基于区域间模拟的不同方法在最近十年中出现，并已在完全开源的工具 TChecker 中实现。基于模拟的方法催生了时间自动机中可达性与活性的高效新算法，并已扩展到更丰富的模型，如加权时间自动机，以及带对角约束与更新的时间自动机。在本文中，我们综述了外推与模拟技术，并讨论了未来的一些开放挑战。