中断时序自动机：验证与表达能力
摘要：中断定时自动机的介绍 中断定时自动机是混合自动机的一个子类，非常适合描述单处理器环境中带有中断的时态多任务系统。虽然混合自动机的可达性问题是不可判定的，但我们证明了对于中断定时自动机而言可达性问题是可判定的。更准确地说，我们证明了中断定时自动机的非时态语言是正则的，通过构建一个有限自动机作为广义类图。然后我们证明，当时钟的数量固定时，中断定时自动机的可达性问题在非指数时间和多项式时间内可解决。为了证明第一个结果，我们定义了中断定时自动机的一个子类ITA-，并证明了(1)任何中断定时自动机都可以被归约到ITA-中一个语言等价的自动机上，(2)在这个子类中的可达性问题在非指数时间内可解决(不需要任何类图)。在下一步中，我们研究了在中断定时自动机上验证实时属性。我们证明了模型检查SCL，即一个时态线性时间逻辑的一个子片段，是不可判定的。另一方面，我们给出了两个时态分支时间逻辑的模型检查过程。我们还比较了经典定时自动机和中断定时自动机的表达能力，并证明了相应的接受语言族是不可比较的。这个结果也适用于由扩展了定时自动机的受控实时自动机（CRTA）所接受的语言。最后，我们将中断定时自动机和CRTA结合起来，构建了一个模型，涵盖了两个类，并证明了可达性问题仍然可判定。此外，我们还证明了中断定时自动机的语言既不是封闭的，也不是与其他语言的交集。
作者：B''eatrice B''erard (LIP6), Serge Haddad (LSV), Mathieu Sassolas (LIP6)
论文ID：1203.6453
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2012-03-30