实时系统的统一模型：符号技术和实现
摘要：广义定时自动机（GTA）模型中，我们考虑了两种类型的时钟，历史时钟和未来时钟，可以简洁地表达许多时态特性，包括定时自动机、具有和不具有对角约束的事件-时钟自动机以及具有计时器的自动机。我们的主要贡献是一种基于模拟的区域算法，用于检查在这个统一模型中的可达性。虽然已经知道这种算法存在于定时自动机中，并且最近已经证明对于没有对角约束的事件-时钟自动机，但这是第一个可以处理具有对角约束的事件-时钟自动机和具有计时器的自动机的结果。我们还为我们的模型提供了一个原型实现，并展示了几个基准测试的实验结果。据我们所知，这不仅是我们统一模型的第一个有效实现，甚至对于具有计时器或没有通过定时自动机经过昂贵的转换到事件-时钟自动机（具有预测时钟）的模型的自动机来说，这也是第一个有效实现。最后但并非最不重要的是，广义定时自动机除了本身有趣之外，还可以用于在定时自动机模型上进行事件-时钟规范的模型检查。
作者：S Akshay and Paul Gastin and R Govind and Aniruddha R Joshi and B Srivathsan
论文ID：2305.17824
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2023-05-30