关于具有输入确定守卫的定时自动机
摘要：计时自动机的广义概念与[DSouza03]的思路一致，具有输入确定性保护，我们展示了它们接受的逻辑框架，包括单调的二阶逻辑特性和具备表达能力的时态逻辑。然后，我们使用Henzinger, Raskin和Schobbens引入的递归运算符的概念来概括这些自动机，并展示了它们也接受了类似的逻辑框架。这些结果是以“逐点”语义为基础的。最后，我们使用这个框架来展示Alur等人的实时逻辑MITL在表达能力上与适当的输入确定性运算符相对应的MSO完备。
作者：Deepak D'Souza, Nicolas Tabareau (PPS)
论文ID：cs/0601096
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23