捕获EMSO逻辑的数据字上的自动机
摘要：对于执行是无限字母表上的单词或部分序列的系统，我们开发了一个通用的规范和实现框架。作为实现模型，我们引入了类寄存器自动机，它是一个带有多个数据值的单向自动机模型。我们的模型结合了寄存器自动机和类内存自动机。它具有自然解释。特别是，它捕捉到了具有无限数量进程并且语义可以描述为一组（动态）消息序列图的通信自动机。在规范方面，我们提供了一个不对变量数量施加任何限制的本地存在单调二阶逻辑。我们研究了实现问题，并展示了该逻辑中的每个公式都可以有效地并且在基本时间内转化为等价的类寄存器自动机。
作者：Benedikt Bollig (LSV)
论文ID：1101.4475
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2012-01-10