Symbolic Register Automata
符号有限自动机和寄存器自动机是有限自动机的两个正交扩展，它们的动机是现实世界中数据可能具有无界域的问题。这些自动机分别解决了对大型或无限字母表模型的需求。这两种自动机模型都有有趣的应用，并且本身就很成功。在本文中，我们介绍了符号寄存器自动机，一个新的模型，结合了符号和寄存器自动机的功能，与以前的应用程序是遥不可及的。我们研究了它们的性质，并提供了空性，包含性和等价性检查的算法，以及实验结果。
2019-05-23 cs.FL
On the Containment Problem for Unambiguous Single-Register Automata with Guessing
寄存器自动机扩展了经典的有限自动机与一组有限的寄存器，可以存储来自一个无限的数据域的数据，为以后的平等比较与数据从一个输入数据字。虽然寄存器自动机的原始模型中的寄存器，在1994年引入的Kaminski和Francez，只能存储数据发生在数据字处理到目前为止，我们在这里研究更有表现力的类寄存器自动机与猜测，寄存器可以nondeterministically采取任何值从无限的数据域，即使这些数据不出现在输入数据字。众所周知，遏制问题，即，对于两个给定的带有猜测A和B的寄存器自动机，判定A接受的语言L（A）是否包含在B接受的语言L（B）中的问题是不可判定的，即使B只使用一个寄存器。我们证明了这个问题是可判定的，如果B是明确的，并使用一个单一的寄存器。
2019-05-28 cs.FL
Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata
本文提出轨道有限集张成的向量空间理论，并据此给出加权寄存器自动机等价性的指数时间判定算法，固定寄存器数时降为多项式时间，同时以相同复杂度改进无歧义寄存器自动机的语言等价性判定。
2024-05-03 cs.FL
Alternating register automata on finite words and trees
我们研究交替寄存器自动机的数据字和数据树的逻辑。数据字（或数据树）是一个字（或树），其每个位置携带来自有限字母表的标签和来自无限域的数据值。我们研究单向自动机与交替控制数据字或树，一个寄存器存储数据和比较它们的平等。这是Demri，Lazic和Jurdzinski开始的研究的延续。从寄存器自动机模型的角度出发，本文的工作有两个目的：（1）简化已有的交替寄存器自动机空性问题的可判定性证明;（2）展示这些模型的可判定扩展。从逻辑的角度来看，我们表明，（a）在数据字的情况下，满足性的LTL与一个寄存器和量化的数据值是可判定的;和（b）满足性的问题，所谓的前向片段的XML文档是可判定的，即使在存在的DTD，甚至是关键的约束。可判定性是通过减少自动机模型介绍。这个片段包含子轴、后代轴、下一个兄弟轴和下一个兄弟轴，以及数据相等和不相等测试。
2012-03-07 cs.DB cs.FL cs.LO
Regular Functions, Cost Register Automata, and Generalized Min-Cost Problems
受正则语言理论在有限状态系统形式化验证中的成功应用的启发，人们重新对发展从字符串到数值的可分析函数理论产生了兴趣，该理论可以为分析有限状态系统的{ \em定量}性质提供基础。在本文中，我们提出了一个确定性的模型关联成本与字符串的参数化操作的兴趣（如添加，缩放，和$\min$），{ \em正则性}的概念，提供了一个衡量表现力的尺度，并研究决策问题和理论性质的成本函数类。我们的规则性的定义依赖于串到树转换器的理论，并允许将成本与以未来事件的规则属性为条件的事件相关联。我们的{ \em成本寄存器自动机}模型允许使用多个“只写”寄存器计算常规函数，这些寄存器的值可以使用允许的操作集进行组合。我们表明，经典的最短路径算法，以及算法设计的计算{ \em折扣成本}，可以采用解决最小成本问题，在我们的模型中指定的功能更一般的类。带有$\min$和增量的成本寄存器自动机给出了一个确定性模型，它等价于{ \em加权自动机}，一个被广泛研究的非确定性模型，这种连接导致了新的见解和新的开放问题。
2012-02-21 cs.FL cs.LO
A Myhill-Nerode Theorem for Register Automata and Symbolic Trace Languages
我们提出了一个新的符号跟踪语义寄存器自动机（扩展的有限状态机），它记录的输入符号，在运行过程中发生的序列，以及输入参数的约束，由这个运行。我们的主要结果是一个推广的经典Myhill-Nerode定理，这个符号设置。我们的推广需要使用三个关系来捕捉寄存器自动机的附加结构。位置等价$\equiv_l$捕获符号轨迹在相同位置结束，转换等价$\equiv_t$捕获它们共享相同的最终转换，并且部分等价关系$\equiv_r$捕获符号值$v$和$v'$分别在符号轨迹$w$和$w'$之后存储在相同寄存器中。如果存在满足一定条件的关系$\equiv_l$，$\equiv_t$和$\equiv_r$，特别是它们都有有限索引，则符号语言被定义为正则语言.我们表明，符号语言相关的寄存器自动机是定期的，我们构造，为每个定期符号语言，一个寄存器自动机，接受这种语言。我们的研究结果提供了一个灰盒学习算法的基础，在设置中，数据参数的约束可以从代码中提取，例如符号/concolic执行或污染的工具。我们相信，转移到灰盒设置是必不可少的，以克服国家的最先进的黑盒学习算法的可扩展性问题。
2021-03-31 cs.FL cs.LO
The Containment Problem for Unambiguous Register Automata
我们调查的复杂性的遏制问题“$L(A)\subseteq L(B)$举行？“，其中$B$是明确的寄存器自动机，而$A$是任意寄存器自动机。我们证明了这个问题是可判定的，并给出了上界的计算复杂性在一般情况下，当$B$被限制为有一个固定数量的寄存器。
2019-01-20 cs.FL
New Techniques for Universality in Unambiguous Register Automata
寄存器自动机是有限自动机，配备了一组有限的寄存器，范围覆盖某些关系结构（如$(\mathbb N;=)$或$(\mathbb Q;<)$）的域。寄存器自动机处理域上的字，并且沿着自动机的运行，寄存器可以存储来自输入字的数据以供稍后比较。众所周知，普遍性问题，即，决定给定寄存器自动机是否接受域上的所有词的问题是不可判定的。最近，我们证明了在2-ExpSpace中，如果所研究的寄存器自动机是在$(\mathbb N;=)$上的并且是无歧义的，即，每个输入单词最多有一次接受运行; Barloy和Clemente不久后将该结果改进为2-ExpTime。在本文中，我们更进一步，证明了问题是在ExpSpace中，并在PSpace中，如果寄存器的数量是固定的。我们的证明是基于新的技术，另外使我们能够表明，问题是在PSpace的单寄存器自动机超过$(\mathbb Q;<)$。作为第三个技术贡献，我们证明了这个问题是可判定的（在ExpSpace）的一个更有表现力的模型，明确的寄存器自动机，其中的寄存器可以采取值nondeterministically，如果定义在$(\mathbb N;=)$和只有一个寄存器使用。
2021-02-16 cs.FL
Weak Cost Register Automata are Still Powerful
我们考虑一个最弱的变种的成本寄存器自动机在热带半环，即无拷贝成本寄存器自动机在$\mathbb{N}$更新使用$\min$和增量。我们表明，该模型可以模拟，在某种意义上，运行计数器机与零测试。我们推断出与该模型相关的一些问题是不可判定的，特别是等价性，从而反驳了2012年的一个猜想。为了强调这些机器有多弱，我们还证明了它们可以表示为线性模糊加权自动机的限制形式。
2018-04-17 cs.FL
A Robust Class of Data Languages and an Application to Learning
我们引入会话自动机，一个处理数据字的自动机模型，即，在一个无限的字母表中。会话自动机支持新数据值的概念，这非常适合于建模协议，其中使用新值的会话是主要兴趣，如安全协议或ad-hoc网络。会话自动机的表达能力与经典的寄存器自动机的表达能力相比有部分扩展，部分减少。我们表明，与寄存器自动机及其各种扩展不同，会话自动机是鲁棒的：它们（i）在交集，并集和（资源敏感）互补下是封闭的，（ii）允许符号正则表示，（iii）具有可判定的包含问题（与寄存器自动机不同），（iv）具有逻辑特征。利用这些结果，我们建立了一个学习算法，通过成员和等价查询来推断会话自动机。
2014-12-27 cs.FL cs.LO
Copyless Cost-Register Automata: Structure, Expressiveness, and Closure Properties
成本寄存器自动机（CRA）及其子类无拷贝CRA是最近由Alfred等人提出的一种新的计算字符串上函数的模型。我们研究了无拷贝CRA的一些结构特性、表现力和闭包特性。我们表明，无拷贝CRA是严格的表达比加权自动机，并没有关闭下反向操作。为了找到一个更好的类，我们对无拷贝CRA施加限制，它以一个新的鲁棒计算模型成功结束，该模型在反向和其他扩展下是封闭的。
2018-04-27 cs.FL
Single use register automata for data words
我们的出发点是数据字的寄存器自动机，采用Kaminski和Francez的风格。我们研究了一次性使用限制的影响，即寄存器在使用后立即清空。我们表明，在单次使用的限制下，自动机理论的数据字变得更加强大。主要结果如下：（a）五种不同的机器模型等价于语言接受者，包括单向和双向单用途寄存器自动机;（b）可以恢复有限字母表上语言的一些代数理论，包括Krohn-Rhodes定理的一个版本;（c）还有一个稳健的换能器理论，具有四个等效模型，包括双向单用途换能器和用于数据字的流串换能器的变型。这些结果与没有单次使用限制的数据字自动机相反，基本上所有模型都是成对不等价的。
2020-05-07 cs.FL
Pumping-Like Results for Copyless Cost Register Automata and Polynomially Ambiguous Weighted Automata
University of Warsaw（华沙大学）；University of Ljubljana（卢布尔雅那大学）；Institute of Mathematics, Physics, and Mechanics (IMFM)（数学、物理和力学研究所）
本文研究了复制less成本寄存器自动机和多项式歧义加权自动机的表达能力，通过泵送序列族工具得出两者在不同域下的泵送样结果，并证明在有理数域下两者不可比较。
2026-01-12 cs.FL
Minimizing Cost Register Automata over a Field
本文利用线性包不变量解决域上代价寄存器自动机的寄存器最小化问题，并推广到状态与寄存器同时最小化及仿射更新情形，同时给出2-ExpTime和NExpTime的复杂度上界。
2024-06-28 cs.FL
Reducing Transducer Equivalence to Register Automata Problems Solved by "Hilbert Method"
在过去的几十年中，代数的经典结果，包括希尔伯特的基本定理，在形式语言中有各种应用，包括Escherichfeucht猜想的证明，HDT0L序列等价的可判定性，以及函数树到串转换器的等价问题的可判定性。在本文中，我们研究了上述代数方法的范围，特别是适用于寄存器自动机的等价问题。我们提供了两个结果，一个阳性，一个阴性。结果表明，无序森林上的MSO变换是等价的。否定的结果来自于尝试将该方法扩展到确定宏树换能器的等效性。我们减少了宏树换能器等价的等价问题，一类寄存器自动机自然相关的我们的方法。然后，我们证明后一个问题是不可判定的。
2019-01-04 cs.FL
Determinisability of register and timed automata
该研究解决了寄存器自动机与时间自动机的确定性成员问题，绘制了完整可判定性图景，并证明在单寄存器/单时钟且输出资源数固定时可判定，其余情况不可判定。
2022-05-09 cs.FL
Complexity Results on Register Pushdown Automata
寄存器下推自动机（RPDA）是经典下推自动机的一种扩展，它以一种受限制的方式处理数据值。RPDA作为一种用于具有数据值的结构化文档的查询语言模型而引起人们的注意。RPDA的成员和空性问题是EXPTIME完全的。本文证明了对于非减和增长的RPDA，成员问题分别成为PSPACE-完全和NP-完全，而空问题对于这些子类仍然是EXPTIME-完全的。
2019-10-23 cs.CC cs.FL
A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Buchi Register Automata
本文将析取 μ↓-演算从有限字重新定义到无限字，并证明其与 Büchi 寄存器自动机表达能力等价。
2024-06-17 cs.FL cs.LO
Bidimensional linear recursive sequences and universality of unambiguous register automata
研究了寄存器自动机在相等数据上的普适性和包含问题。我们表明，通用性和包含问题可以解决2-EXPTIME复杂性时，输入自动机是没有猜测和明确的，目前最有名的2-EXPSPACE上限由Mottet和Mittas的改进。当两个自动机的寄存器数目固定时，我们得到了较低的EXPTIME复杂度，也改进了Mottet和Rumas在寄存器数目固定时的EXPSPACE上界。我们把包容性归结为普适性，然后把普适性归结为计算自动机运行轨道数的问题。我们发现，轨道计数函数满足系统的二维线性递归方程与多项式系数（linrec），这概括了类似的递归的第二类斯特林数，然后我们表明，普遍性降低到零的linrec序列的问题。虽然这样的计数方法是经典的，并已成功地应用于明确的有限自动机和文法在有限的字母表，其应用程序注册自动机在无限的字母表是新颖的。给出了两个判定由轨道计数函数产生的二维线性递归序列的无零性问题的算法。这两种算法都依赖于线性非交换代数的技术。第一个算法执行变量消除，并具有基本的复杂性。第二个算法是第一个算法的改进版本，它依赖于斜多项式域上矩阵的Hermite范式的计算。第二个算法产生一个EXPTIME决策过程的linrec序列的零问题，这反过来又产生了声称的范围的寄存器自动机的普遍性和包含问题。
2021-01-04 cs.FL
A Linear-Time Nominal $μ$-Calculus with Name Allocation
无限字母表语言的逻辑和自动机模型，如Freeze LTL和寄存器自动机，用于验证过程或带有数据的文档。它们与名义集上的形式主义密切相关，例如非确定性轨道有限自动机（NOFA），其中名称扮演数据的角色。在这种形式主义中的推理问题在计算上往往是困难的。名字绑定的名义自动机模型，如规则的非确定性名义自动机（RNAs）已被证明是计算上更容易处理。在本文中，我们介绍了一个线性时间不动点逻辑Bar-muTL有限字在一个无限的字母表，它的特点是完全否定和冻结量化通过名称绑定。我们通过对扩展的正则非确定性名义自动机的非平凡约简表明，尽管Bar-muTL允许无限制的非确定性和无限多的寄存器，但RNAs上的模型检验Bar-muTL和可满足性检验都具有基本的复杂性.例如，模型检验在2 ExpSpace中，更准确地说是在参数化的ExpSpace中，有效地将寄存器的数量作为参数。
2021-08-20 cs.FL cs.LO
Runtime Verification Based on Register Automata
我们提出了TOPL自动机作为一种新的方法，运行时验证的系统与无限的资源生成。典型的这种系统是面向对象的程序，它可以在执行过程中动态地生成无限数量的新对象标识。我们的形式主义是基于寄存器自动机，一个特别成功的方法，在自动机在无限的字母表管理有限状态机有界许多输入存储寄存器。我们表明，TOPL自动机是同样的表达注册自动机，但适合表达程序的属性。与其他运行时验证方法相比，我们的技术可以处理当前工具无法处理的一类属性。我们特别表明，需要值更新的属性是无法用当前的技术来表达的，但自然被TOPL机器捕获。在实践方面，我们提出了一个工具，通过TOPL属性，覆盖率和监控系统的开销之间的权衡是可调的，通过一些参数的Java程序的运行时验证。我们通过检查涉及多个对象的属性和大型开源项目上的值链来验证我们的技术。
2015-01-20 cs.FL cs.SE
Synchronizing Data Words for Register Automata
寄存器自动机（Register Automata，RA）是一种用有限寄存器扩展的有限自动机，用于存储和比较来自无限域的数据。我们研究的概念，在RA同步数据字：是否存在一个数据字，发送所有状态的RA到一个单一的状态？对于具有k个寄存器的确定性RA（k-DRA），我们证明了从无限数据域输入具有2k+1个不同数据的数据字足以同步。我们证明了DRA的同步问题在一般情况下是PSPACE完全的，而对于1-DRA是NLOGSPACE完全的。对于非确定性RA（NRA），我们表明，阿克曼（n）不同的数据（其中n是RA的大小）可能是必要的同步。NRA的同步问题通常是不可判定的，然而，我们建立了1-NRA的Ackerman-完全性问题。另一个主要结果是NEXPTIME完整性的长度有界的NRA的同步问题，其中的同步数据字的长度上的限制，写在二进制，给出。这最后一个结构的一个变体允许证明NRA的长度有界的普遍性问题是co-NEXPTIME-完备的。
2019-06-09 cs.FL
Symbolic Register Automata for Complex Event Recognition and Forecasting
National and Kapodistrian University of Athens（雅典国立与卡波季斯特里亚大学）；National Center for Scientific Research “Demokritos”（德谟克利特国家科学研究中心）；University of Piraeus（比雷埃夫斯大学）
我们提出了一个自动机模型，它是符号自动机和寄存器自动机的组合，即，我们用记忆来丰富符号自动机。我们称这种自动机为符号寄存器自动机（SRA）。SRA扩展了符号自动机的表达能力，允许布尔公式不仅应用于从输入字符串读取的最后一个元素，而且应用于存储在其寄存器中的多个元素。SRA还扩展了寄存器自动机，允许任意布尔公式，除了等式谓词。我们研究了SRA在并、交、连接、Kleene闭包、补和确定性下的闭包性质，并证明了SRA与符号自动机相反，在补下一般不是闭的，也不是可确定的.但是，当使用窗口操作符（复杂事件识别中的典型操作）时，它们在这些操作下关闭。我们展示了如何SRA可以用于复杂事件识别，以检测事件流的模式，使用我们的框架，提供声明性和成分语义，并允许系统处理这样的自动机。我们还展示了如何SRA的行为，因为他们消费的事件流，可以给出一个概率描述的帮助下，预测后缀树。这使我们能够从复杂事件识别到复杂事件预测，在复杂事件预测中，除了检测复杂模式外，我们还可以有效地预测它们的发生。
2021-10-08 cs.AI cs.DB cs.FL
An Automata-Theoretic Approach to the Verification of Distributed Algorithms
我们介绍了一个自动机理论的方法验证分布式算法上运行的环形网络。在分布式算法中，任意数量的进程协作以实现共同的目标（例如，选一个领导人）。进程拥有来自无限全序域的唯一标识符（pids）。算法在同步循环中进行，每一循环允许进程执行有界的动作序列，例如发送或接收pid，将其存储在某个寄存器中，并比较寄存器内容wrt。相关的总订单。算法应该是正确的，与进程的数量无关。为了指定正确性属性，我们引入了一个可以推理进程和pid的逻辑。关于领导者选举，可以说，在执行结束时，每个进程将最大pid存储在某个专用寄存器中。由于分布式算法的验证是不可判定的，我们提出了一种欠近似技术，它限制了轮数。这是一种很有吸引力的方法，因为分布式算法得出结论所需的轮数通常比进程数呈指数级小。我们提供了一个自动机理论的解决方案，减少模型检验空交替双向自动机的话。总的来说，我们表明，在环上的分布式算法的圆形有界验证是PSPACE完成的。
2015-04-24 cs.FL cs.LO
History-Register Automata
程序与动态分配能够创建和使用无限数量的新鲜资源，如引用，对象，文件等，我们提出了历史寄存器自动机（HRA），一个新的自动机理论的形式主义建模这样的程序。HRA扩展了以前方法的表达能力，并使我们达到了可达性检查的可判定性极限。我们的机器的显着特点是它们使用无限的记忆集（历史），输入的符号可以有选择地存储和比较的符号遵循。此外，存储的符号可以通过重置来消耗或删除。我们表明，消费和复位功能的组合，使自动机足够强大，以模仿计数器机，并在所有常规操作下，除了互补收益率关闭。此外，我们还研究了较弱的概念HRAs之间的表现力和有效性的不同的平衡。
2016-03-29 cs.FL cs.PL
The single-use restriction for register automata and transducers over infinite alphabets
University of Warsaw（华沙大学）；University College London（伦敦大学学院）
本论文研究了无穷字母表上寄存器自动机与转换器的单次使用限制，证明了该限制下各类自动机与转换器模型的表达能力等价性，并提供了连贯的叙述与代数模型。
2024-06-27 cs.CL cs.FL
Church Synthesis on Register Automata over Linearly Ordered Data Domains
本文研究线性有序数据域上寄存器自动机规范的Church综合，提出单侧Church博弈并证明其可判定性（ExpTime），并应用于换能器综合。
2023-06-22 cs.FL
Symbolic ω-automata with obligations
本文提出了一种基于义务的符号ω-自动机，通过引入义务构造来处理无限字母表下的转移信息，扩展了传统ω-自动机的表达能力。
2025-12-02 cs.FL cs.LO
Synthesis and Verification of Register Automata over Data Sequences (Technical Report)
National Chengchi University（国立成功大学）；University of Kaiserslautern-Landau（凯撒斯劳滕-劳恩堡大学）；University of Liverpool（利物浦大学）
本文提出了一种从神经网络中提取鲁棒寄存器自动机的方法，通过结合鲁棒性检查器与自动机学习算法，实现对神经网络的鲁棒性评估。
2026-10-22 cs.AI cs.FL cs.LG
A Generic Solution to Register-bounded Synthesis with an Application to Discrete Orders
我们研究的反应系统与环境相互作用的合成使用一个无限的数据域。一个流行的形式主义指定和建模这样的系统是注册自动机和传感器。它们通过添加寄存器来存储数据值并将传入的数据值与存储的数据值进行比较来扩展有限状态自动机。从不确定或通用寄存器自动机合成一般是不可判定的。然而，其寄存器有界变体，其中另外给出了所寻找的转换器中寄存器数量的界限，已知对于可以比较数据是否相等的通用寄存器自动机是可判定的，即，用于数据域$(N,=)$。本文将可判定性边界推广到线性阶自然数域$(N,<)$。我们的解决方案是通用的：我们定义了一个充分条件的数据域（经常逼近）的可判定性的寄存器有界合成。自然数据域（如$(N,<)$）满足该条件。它允许人们使用简单的语言理论论证，避免技术博弈论推理。此外，通过定义一个通用的概念之间的数据域的reductionary，我们显示的可判定性的合成在域$(N^d,<^d)$的元组的号码配备了组件明智的偏序和域$(Σ^*,\prec)$的有限字符串的前缀关系。
2022-06-08 cs.FL
Symbolic Automata with Memory: a Computational Model for Complex Event Processing
我们提出了一个自动机模型，它是符号自动机和寄存器自动机的组合，即，我们用记忆来丰富符号自动机。我们称这种自动机为寄存器匹配自动机（RMA）。RMA扩展了符号自动机的表达能力，允许公式不仅应用于从输入字符串读取的最后一个元素，而且应用于存储在其寄存器中的多个元素。RMA还扩展了寄存器自动机，除了等式谓词之外，还允许任意公式。我们研究的封闭性下联盟，级联，Kleene+，补充和确定性的RMA，相反，符号自动机，是不确定的识别时，不考虑输出的过渡考虑。然而，当使用窗口操作符（复杂事件处理中的一个典型特征）时，RMA即使被视为识别器也确实是可确定的。我们提出了详细的算法构造确定性RMA从正则表达式扩展$n$ -ary约束。我们展示了如何RMA可以用于复杂事件处理，以检测事件流的模式，使用一个框架，提供指称和成分语义，并允许系统处理这样的自动机。
2018-06-11 cs.DB cs.FL
Alternating Automata on Data Trees and XPath Satisfiability
数据树是一个无序的有序树，它的每个节点都由一个来自有限字母表的字母和一个来自无限集合的元素（“数据”）标记，其中后者只能比较相等。本文考虑了数据树上的交替自动机，它可以向下移动和向下移动，并且有一个寄存器用于存储数据。主要结果是：有限数据树上的非空性是可判定的，但不是原始递归的;安全自动机的非空性是可判定的，但不是初等的。证明使用不确定树自动机与故障计数器。允许向上移动、向下移动或两个寄存器，每一个都会导致不可判定性。作为推论，可判定性获得两个数据敏感片段的XML查询语言。
2010-06-14 cs.DB cs.FL cs.LO
A Generic Solution to Register-bounded Synthesis with an Application to Discrete Orders
我们研究的反应系统与环境相互作用的合成使用一个无限的数据域。一个流行的形式主义指定和建模这样的系统是注册自动机和传感器。它们通过添加寄存器来存储数据值并将传入的数据值与存储的数据值进行比较来扩展有限状态自动机。从不确定或通用寄存器自动机合成一般是不可判定的。然而，其寄存器有界变体，其中另外给出了所寻找的转换器中寄存器数量的界限，已知对于可以比较数据是否相等的通用寄存器自动机是可判定的，即，对于数据域（N，=）。本文将可判定性边界推广到线性阶自然数的定义域（N，<）.我们的解决方案是通用的：我们定义了一个充分条件的数据域（经常逼近）的可判定性的寄存器有界合成。自然数据域（如（N，<））满足该条件。它允许人们使用简单的语言理论论证，避免技术博弈论推理。此外，通过定义一个通用的概念之间的数据域的约简，我们证明了在域（N^d，<^d）的元组的号码配备了组件的偏序和域（N ^*，\prec）的有限字符串的前缀关系的合成的可判定性。
2022-05-20 cs.FL
Alternating Nominal Automata with Name Allocation
针对无限字母表自动机推理难的问题，提出带名称分配的正则交替名义自动机，证明其寄存器无界时非空与包含问题仍为初等复杂度，可近乎完全去交替，并将Bar-μTL某分支模型检测复杂度提升一个指数级。
2025-05-19 cs.FL
The boundedness and zero isolation problems for weighted automata over nonnegative rationals
我们考虑非负有理数半环上的线性代价寄存器自动机（等价于加权自动机），它推广了概率自动机。有界性和零隔离这两个问题是问是否存在一个分别收敛到无穷大和零的单词序列。在一般模型中，这两个问题都是不可判定的，所以我们把重点放在无拷贝线性约束上。在那里，我们证明了有界性问题是可判定的。至于零隔离问题，我们需要进一步限制类。我们得到一个模型，零隔离成为等同于普遍覆盖的orthant矢量加法系统（OVAS），一个新的模型在VAS家庭有趣的本身。在标准VAS中，仅在正正体中考虑运行，而在OVAS中，每个正体都有其自己的一组可以应用于该正体的向量。假设Schanuel的猜想是正确的，我们证明了三维OVAS的通用覆盖性的可判定性，这意味着在一个最多有三个独立寄存器的模型中零隔离的可判定性。
2022-05-26 cs.FL cs.LO
Nominal Tree Automata With Name Allocation
针对数据树自动机语言包含判定难的问题，提出基于nominal集合与显式名称分配的树自动机模型，支持非确定性与任意寄存器数，且语言包含检查为参数化指数时间的初等复杂度。
2024-07-11 cs.FL
An automaton over data words that captures EMSO logic
我们开发了一个通用的框架，其执行系统的规范和实施的话，或偏序，在一个无限的字母表。作为一个模型的实现，我们引入类寄存器自动机，一个单向自动机模型的话多个数据值。我们的模型结合了寄存器自动机和类记忆自动机。它有自然的解释。特别是，它捕获通信自动机与无限数量的进程，其语义可以被描述为一组（动态）消息序列图。在规范方面，我们提供了一个局部存在一元二阶逻辑，不对变量的数量施加任何限制。我们研究的可实现性问题，并表明，从逻辑的每一个公式可以有效地，并在小学的时间，翻译成一个等价的类寄存器自动机。
2011-06-10 cs.FL
Unambiguisability and Register Minimisation of Min-Plus Models
Department of Computer Science, Technion, Israel（以色列理工学院计算机科学系）
本文研究了最小-最大自动机的无歧义性问题和热带成本寄存器自动机的反最小化问题，证明了前者可判定而后者不可判定。
2026-04-29 cs.FL
Scalable Tree-based Register Automata Learning
本文提出可扩展的寄存器自动机学习算法$SL^λ$，通过基于树的数据结构和短受限测试机制大幅减少测试数量，并在RALib中实现，实验表明其性能优于现有最先进算法$SL^*$。
2024-01-25 cs.FL
Grey-Box Learning of Register Automata
模型学习（Model Learning）主动自动机学习）是用于获得软件组件的黑盒有限状态模型的高效技术。到目前为止，推广到具有携带数据参数的输入/输出的无限状态系统一直具有挑战性。现有的无限状态系统的模型学习工具面临可扩展性问题，只能应用于有限类的系统（寄存器自动机与平等/不平等）。在本文中，我们展示了如何通过从运行中提取输入和输出参数的约束，并将这些灰盒信息提供给学习者，来提高模型学习技术的性能。更具体地说，我们提供了新的实现的树Oracle和等价Oracle从RALib，它使用派生的约束。我们使用一个现有的Python污染库从Python程序的运行中提取约束，并在几个基准测试中将我们的RALib灰盒版本与现有的黑盒版本进行比较，包括Python标准库中的一些数据结构。我们的原理验证实现结果在发送到软件系统的输入数量方面几乎有两个数量级的改进。我们的方法可以推广到更丰富的模型类，也使RALib能够学习黑盒技术无法达到的模型，例如组合锁。
2020-09-21 cs.FL
Two-way affine automata can verify every language
本文研究双向仿射有限自动机在 Arthur-Merlin 验证中的能力，提出单寄存器弱验证与双寄存器强验证协议，证明其能以单指数期望时间有界误差验证所有二元及 r 元语言。
2025-02-18 cs.FL
Undecidability of Reachability for Constraint Automata
University of Wrocław（弗罗茨瓦夫大学）
该研究证明有限二进制字上的约束自动机可达性不可判定，8个寄存器即可实现，还推导了相关非空性问题的不可判定性，同时确定了特定布尔守卫下Büchi非空性及前缀-后缀LTL可满足性的PSPACE完全性。
2026-10-14 cs.FL
Streamable Regular Transductions
出于实时监控和数据处理应用程序，我们开发了一个正式的理论定量查询流数据，可以有效地进行评估。我们考虑明确的成本寄存器自动机（CRA），这是一个有限的状态控制（用于识别规则模式）与一组有限的数据寄存器（用于计算数值聚集）相结合的机器的模型。CRA的定义由可以应用于寄存器的数值运算的集合参数化。这些机器产生了可流式正则转换（SR）类，以及当寄存器更新是无拷贝时的可流式线性正则转换（SLR）类，即每个寄存器最多出现一次更新的右手侧表达式。我们给出了类SR的逻辑特征（分别为，SLR）使用从字符串到DAG（分别为，树）没有向后的边缘。此外，我们建立了两个类SR和SLR下的操作是相关的设计查询语言关闭。最后，我们研究了与加权自动机（WA）的关系，并表明，CRA在一个适当选择的操作集对应于WA，从而建立WA是一个特殊的情况下的CRA。
2019-11-03 cs.FL cs.LO
Supported Sets -- A New Foundation For Nominal Sets And Automata
本工作提出并讨论了支持集的范畴，它为各种名义集提供了统一的基础，如相等对称集、序对称集和重命名集。我们表明，所有这些不同的口味类别的名义集是一元的支持集。因此，支持集提供了一种规范的有限方式来表示名义集和其中的自动机，例如寄存器自动机。支持集合中的名称绑定由遵循de Bruijn索引思想的函子建模。这个函子提升到著名的抽象函子在名义集。与单子性结果一起，这产生了一个转换过程，该过程在支持集上采用寄存器自动机的有限表示，并将其转换为标称集上的配置自动机。
2022-10-05 cs.FL
Feasible Automata for Two-Variable Logic with Successor on Data Words
我们介绍了一个自动机模型的数据字，这是在每个位置进行一个符号从一个有限的字母表和一个值从一个无界的数据域的话。该模型是（语义）的数据自动机，介绍了Bojanczyk，等的限制。在2006年，它被称为弱数据自动机。它的表达能力比数据自动机差，而表达能力又是寄存器自动机无法比拟的。弱数据自动机的表达能力与后继为+1且数据值相等\sim，EMSO 2（+1，\sim）的存在一元二阶逻辑完全对应。它遵循从以前的工作，大卫，等。等人在2010年提出了弱数据自动机的非空性问题可以在2-NEXPTIME中判定。此外，我们还研究了数据ω-串上的弱Büchi自动机。它们可以用EMSO 2（+1，\sim）的扩展来刻画，其中存在量词用于无限集合.最后，通过对弱数据自动机的非空性问题进行非确定性多项式时间约简，得到了其非空性问题的复杂性界。
2011-10-06 cs.FL cs.LO
On Streaming String Transducers and HDT0L Systems
R.在2010年，P.Cerny和P.Cerny提出了一个单向确定性自动机模型来定义有限字符串的转换。无拷贝SST用一组寄存器扩展确定性有限状态自动机，在其中存储中间输出串，并且这些寄存器可以以线性方式沿着运行进行组合和更新，即，在转换时不能复制寄存器内容。众所周知，无拷贝SST精确地捕获了由B. Courcelle和确定性双向换能器的表达相同。它们具有良好的算法特性。最值得注意的是，它们有可判定的等价问题（在PSpace中）。在本文中，我们表明，他们仍然有可判定的等价问题，即使没有复制的限制。证明减少到HDT0L序列等价问题，这是已知的可判定的。我们还表明，后者的问题是困难的SST等价问题，模线性时间减少。
2014-12-01 cs.FL cs.LO
Reachability Analysis of Reversal-bounded Automata on Series-Parallel Graphs
字符串上的有限状态自动机的扩展，如多头自动机或多计数器自动机，已成功地用于编码许多无限状态非正则验证问题。在本文中，我们考虑一个推广的自动机理论的无限状态验证从字符串标记串并行图。我们定义了一个模型的非确定性，2路，并发自动机工作串并行图和通信通过共享寄存器的节点上的图形。我们考虑以下验证问题：给定一个系列的串并行图描述的上下文无关的图转换系统（GTS），并在串并行图的并发自动机，是一些图所产生的GTS接受的自动机？一般的问题是不可判定的已经（单向）多头自动机字符串。我们表明，一个有界的版本，其中自动机使固定数量的反转沿图，并使用固定数量的共享寄存器是可判定的，即使有没有约束的GTS生成的串并行图的大小。我们的可判定性结果是基于建立上下文切换的数量是有界的，并对有界并发自动机的计算进行编码，以将空性问题减少到下推自动机的空性问题。
2015-09-24 cs.FL
Extended Models of Finite Automata
在文献中提出的许多自动机模型可以被看作是一个有限自动机配备了一个额外的存储机制。在这篇论文中，我们主要研究了两个这样的模型，即群上的有限自动机和归巢向量自动机。群$ G $上的有限自动机是配备有保持群$ G $的元素的寄存器的非确定性有限自动机。寄存器被初始化为群的单位元素，并且如果在每一步与群元素相乘之后，寄存器等于计算结束时的单位元素，则计算成功。我们调查的语言识别能力的有限自动机在整数和有理矩阵组，并揭示了新的语言类之间的关系，这些模型。我们研究了各种参数对语言识别能力的影响。我们建立了矩阵半群的决策问题和相应的自动机之间的联系。给出了关于价下推自动机和上下文无关价文法的一些新结果。我们还提出了新的归巢向量自动机模型，这是一个有限自动机配备了一个向量，可以乘以一个矩阵在每一步。可以检查向量是否与初始向量等效，并且验收标准最终处于接受状态，其中向量的值等于初始向量。我们研究的效果，各种限制的模型，限制矩阵到一个特定的集合，并允许等价性测试只在计算结束时。我们定义了模型的不同变体，并将其语言识别能力与经典模型进行了比较。
2019-12-25 cs.FL
Star Complexity of Parikh Images of Languages over Infinite Alphabets
Technion – Israel Institute of Technology（以色列理工学院）
研究无限字母集上语言的Parikh图像的星复杂度，证明单寄存器自动机识别语言的Parikh图像星高上限为2，并反驳多寄存器情况下关于上下文无关文法与无限字母自动机表达能力等价的猜想。
2026-05-10 cs.FL
Model Checking Flat Freeze LTL on One-Counter Automata
本文解决了单计数器自动机上平坦冻结线性时序逻辑模型检测的可判定性开放问题，通过归约到带参数化相等性测试的可达性问题并转化为Presburger算术证明其可判定。
2018-12-06 cs.FL cs.LO
On the expressiveness of Parikh automata and related models
Parikh有限词自动机（PA）是Klaedtke和Ruess在2003年提出并研究的。PA的自然变体产生于将PA等效地视为自动机，该自动机保持其转换的计数并半线性地约束其数量。在这里，我们采用这种观点，并定义仿射PA（APA），它通过每个转换在PA寄存器上引起仿射变换来扩展PA，以及字母上的PA（LPA），它通过迫使同一字母上的任何两个转换同等地影响寄存器来限制PA。然后，我们报告的表现力，封闭性和可判定性等PA的变种。我们注意到，确定性PA严格弱于确定性反向有界计数器机器。我们开发泵式引理，并确定一个明确的PA语言没有确定性PA。
2011-07-02 cs.FL
Decidability of Timed Communicating Automata
研究了时间通信网络的可达性问题。每个进程都是一个时间自动机，通过在无界FIFO通道上交换消息与其他进程进行通信。消息携带时钟，该时钟在发送和接收时以适当的定时约束进行检查。每个自动机只能访问它的本地时钟和发送/接收消息的消息时钟集。时间是密集的，所有的时钟都以相同的速度进化。我们的主要贡献是一个完整的特征的可判定和不可判定的通信拓扑结构概括和统一以前的工作。从技术的角度来看，我们使用量词消去和减少计数器自动机与寄存器。
2018-04-20 cs.DC cs.FL cs.LO
Complexity of Membership and Non-Emptiness Problems in Unbounded Memory Automata
本文研究ν-自动机、分层记忆自动机和历史寄存器自动机三类无界记忆自动机的复杂性，证明其成员资格问题均为NP完全，并证明ν-A的非空性问题是PSPACE完全的，区别于HRA的Ackermann完全性。
2023-07-07 cs.FL
Complex Event Recognition with Symbolic Register Transducers: Extended Technical Report
Institute of Informatics & Telecommunications, National Center for Scientific Research “Demokritos”（希腊德谟克利特国家科学研究中心信息学与电信研究所）；Department of Maritime Studies, University of Piraeus（比雷埃夫斯大学海事研究系）
本文提出基于符号寄存器转换器（SRT）的复杂事件识别系统，通过结合符号自动机与寄存器自动机提供清晰语义，并证明其在窗口算子下封闭，实验表明该系统比现有方法表达力更强且更高效。
2024-07-03 cs.AI cs.DB cs.FL
