事件时钟自动机的模拟
摘要：事件时钟自动机是一种著名的时态自动机子类，具有良好的理论性质，如确定性，并且在实践中用于捕捉时态规范。然而，与时态自动机不同的是，目前没有事件时钟自动机的实现。这主要是因为将时区算法适应到事件时钟自动机的环境中具有困难。这个困难最近在[Geeraerts et al 2011,2014]中得到研究，作者提出使用时区外推来解决这个问题。 在本文中，我们提出了一个不同的基于时区算法来解决事件时钟自动机的可达性问题，使用有限模拟。我们结果的一个令人惊讶的后果是，在仅使用预言时钟的事件预测自动机子类中，我们甚至在没有任何模拟的情况下获得有限性。对于一般的事件时钟自动机，我们的新算法利用了G-模拟框架，这是已知的达到可达性的最粗糙的模拟关系，并且最近已经在时态自动机的其他扩展中取得进展。
作者：S Akshay, Paul Gastin, R Govind, B Srivathsan
论文ID：2207.02633
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2022-11-30