时间自动机与信号自动机互模拟算法：模型验证的新途径

本文主要探讨了时间自动机与信号自动机在实时系统模型验证中的重要性和相互关系。时间自动机，由Alur等人提出，作为一种被广泛应用的工具，用于计算机软硬件和网络协议的实时性质模型验证。这类自动机的核心概念是时间事件，其转换过程假设所有事件瞬间完成，时间在状态转移之间流逝。 然而，对于信号自动机而言，它是一种更为适合某些实时系统模型的表示方式。信号自动机引入了"分离信号"的概念，这意味着状态转换在特定的时间区间内完成，并且整个过程中时间约束必须得到满足。这种特性使得信号自动机在反映实际系统的实时性方面更具优势，但遗憾的是，尽管理论上有其独特价值，目前尚缺乏有效的验证算法。 作者朱维军针对这一问题，研究了时间自动机与信号自动机之间的关系，并提出了一种关键的互模拟算法。通过证明两者识别语言的能力相同，以及它们之间的双向模拟关系，作者构建了一个将时间自动机验证算法应用到信号自动机验证问题上的桥梁。这一算法线性且直观，将现有的时间自动机验证技术与信号自动机的优势相结合，使得基于信号自动机的模型验证变得可行和实用。 互模拟算法的提出不仅填补了现有技术的空白，而且对实时系统建模和验证领域产生了重要影响。该算法的实施意味着信号自动机可以借助成熟的时间自动机验证工具进行验证，从而提高了模型验证的效率和准确性。因此，本文的工作对于推动实时系统模型验证技术的发展，特别是在工业界的应用，具有显著的实际意义。 关键词包括：时间自动机、信号自动机、离散步长双向模拟、模型验证，这些关键词揭示了论文的核心内容和研究焦点，即如何通过理论创新解决实际问题，促进实际应用的发展。这篇文章是一项理论与实践相结合的重要贡献，对于理解并优化实时系统模型验证方法具有深远影响。