摘要

信号自动机为一类实时系统建立了比时间自动机更适合的模型.文中针对信号自动机因无验证算法可用而不能用于实际的实时系统模型验证的问题,把信号自动机验证归约到时间自动机验证,证明了两种自动机具有相同的识别语言能力,并具有双向模拟关系.在此基础上提出了线性的互模拟算法,把互模拟算法和已有的时间自动机验证算法结合起来,得到了信号自动机的验证算法,从而解决了对信号自动机模型的验证问题.