具名Büchi自动机与名称分配
摘要：无穷字母表上的无穷字既可以作为资源分配和再利用在线性时间上的时间发展模型。我们在名义集的设置中研究无穷字母表上的ω-语言，并研究无限栏字符串的语言，即特征新名称绑定的名称的无限序列；绑定粗略对应于在带有寄存器的自动机模型中从输入字中读取字母。我们引入正则名义非确定布基自动机（布基RNNAs），这是一种用于无限栏字符串语言的自动机模型，改造了先前引入的有限栏字符串的RNNAs。我们的机器具有显式绑定（即资源分配）转换，并通过布基式接受条件处理其输入。它们是从名义集的名义绑定的抽象视角中产生的。作为我们的主要结果，我们证明与大多数其他无限字母表上的非确定自动机模型相反，布基RNNAs的语言包含性决策是可判定的，事实上是基本的。这使布基RNNAs成为模型检查中的合适工具。
作者：Henning Urbat and Daniel Hausmann and Stefan Milius and Lutz Schr"oder
论文ID：2107.03213
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2021-07-13