论文标题
定时自动机的基于区域的验证：外推，仿真等等？
Zone-based verification of timed automata: extrapolations, simulations and what next?
论文作者
论文摘要
Rajeev Alur和David Dill在90年代初引入了定时自动机。在过去的几十年中，定时自动机已成为实时系统验证的事实上的模型。定时自动机的算法基于使用区域作为符号表示的状态空间的遍历。由于状态空间是无限的，因此终止依赖于有限的抽象，这些抽象产生了可及状态的有限表示。 获得有限抽象的第一个解决方案是基于区域的外推，并且已在行业强度工具Uppaal中实施。在过去的十年中，基于区域之间的模拟进行了不同的方法，并已在Tchecker完全开源工具中实施。基于仿真的方法为定时自动机的可及性和可及性带来了新的有效算法，并且还扩展到了更丰富的模型，例如加权定时自动机，以及具有对角线约束和更新的定时自动机。 在本文中，我们调查了外推和仿真技术，并讨论了未来的一些开放挑战。
Timed automata have been introduced by Rajeev Alur and David Dill in the early 90's. In the last decades, timed automata have become the de facto model for the verification of real-time systems. Algorithms for timed automata are based on the traversal of their state-space using zones as a symbolic representation. Since the state-space is infinite, termination relies on finite abstractions that yield a finite representation of the reachable states. The first solution to get finite abstractions was based on extrapolations of zones, and has been implemented in the industry-strength tool Uppaal. A different approach based on simulations between zones has emerged in the last ten years, and has been implemented in the fully open source tool TChecker. The simulation-based approach has led to new efficient algorithms for reachability and liveness in timed automata, and has also been extended to richer models like weighted timed automata, and timed automata with diagonal constraints and updates. In this article, we survey the extrapolation and simulation techniques, and discuss some open challenges for the future.
