Single use register automata for data words
我们的出发点是数据字的寄存器自动机，采用Kaminski和Francez的风格。我们研究了一次性使用限制的影响，即寄存器在使用后立即清空。我们表明，在单次使用的限制下，自动机理论的数据字变得更加强大。主要结果如下：（a）五种不同的机器模型等价于语言接受者，包括单向和双向单用途寄存器自动机;（b）可以恢复有限字母表上语言的一些代数理论，包括Krohn-Rhodes定理的一个版本;（c）还有一个稳健的换能器理论，具有四个等效模型，包括双向单用途换能器和用于数据字的流串换能器的变型。这些结果与没有单次使用限制的数据字自动机相反，基本上所有模型都是成对不等价的。
2020-05-07 cs.FL
On the capabilities of grammars, automata, and transducers controlled by monoids
在过去的几十年里，语言理论中的经典模型已经被幺半群定义的控制机制所扩展。我们研究的么半群的原因扩展的上下文无关文法，有限自动机，或有限状态转换器，以超过原来的模型的能力。此外，我们调查时，在扩展的自动机模型中，不确定性的变体不同于确定性的能力。我们表明，所有这些条件实际上是等价的，并提出了一个代数特征。特别是，开放的问题，是否每一种语言所产生的价文法在有限幺半群是上下文无关的提供了一个肯定的答案。
2011-03-17 cs.FL math.GR
Proceedings Second International Workshop on Trends in Tree Automata and Tree Transducers
本卷包含在2013年10月19日在越南河内举行的第二届国际树自动机和传感器趋势研讨会（TTATT 2013）上发表的论文。讲习班与ATVA核查会议在同一地点举行。第一期研讨会与区域技术援助机构在同一地点举行，地点在日本名古屋。研讨会的兴趣在于程序设计语言、验证和数据库理论的交叉点，这些都是树自动机和传感器最近应用的领域。
2013-11-20 cs.FL cs.LO cs.PL
On Transition Constructions for Automata -- A Categorical Perspective
本文从范畴论视角研究确定性自动机的转移幺半群构造，将其确立为伴随关系并推导出与等式和余等式集合相关的单子与余单子，同时为 lasso 和 Ω-automata 提供了构成伴随关系的类似转移代数构造。
2024-06-27 cs.FL
CALF: Categorical Automata Learning Framework
自动机学习是一种已成功应用于验证的技术，自动机类型根据应用领域而变化。自动机学习算法的适应性越来越复杂的自动机类型必须从头开始开发，因为没有抽象的理论提供指导。这使得设计这样的算法变得困难，并且模糊了它们的正确性证明。我们介绍了一个简单的范畴理论的形式主义，提供了一个适当的抽象的基础，研究自动机学习。此外，我们的框架建立了学习，测试和最小化算法之间的正式关系。我们说明了它的一般性与两个例子：确定性和加权自动机。
2017-06-26 cs.FL
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
Finite-State Transducers in the Wheeler Setting
University of Udine (DMIF), Italy（乌迪内大学）
本文提出顺序 Wheeler 转换器，结合底层自动机的 Wheeler 条件与输出函数的单调性，证明其封闭性、极小化理论及 Myhill-Nerode 风格定理，刻画可实现的函数类。
2026-08-14 cs.FL
On Constructing Finite Automata by Relational Programming
针对博弈程序需以可被代数工具分析的低级数学格式表示的需求，提出用关系编程工具构造能实现给定输入输出对集合的最小转换器，解决经典有限状态自动机优化技术不适用的问题。
2025-02-12 cs.FL
Active Learning of Deterministic Transducers with Outputs in Arbitrary Monoids
本文基于范畴框架研究了任意幺半群输出的确定性转换器，给出了最小转换器存在且唯一的充要条件，并利用成员与等价查询提供了学习该转换器的抽象算法及实现讨论。
2025-10-08 cs.FL
A geometric approach to (semi)-groups defined by automata via dual transducers
通过逆变换器的丰富对偶的概念，我们给出了由自动机定义的群的一种几何方法。利用这种几何对应，我们首先提供了一些有限性结果，然后我们考虑群生成的Cayley型机的对偶。最后，我们解决的问题，这些集团在边界上的行动的研究。我们表明，具有基本上自由的行动，没有临界点的团体的例子在于由换能器的丰富的对偶生成一个扭自由半群定义的组的类。最后，我们给出了边界上有有限Schreier图的充要条件，从而证明了判定边界上基数上界为某个固定整数的Schreier图的算法问题的可判定性.
2014-03-07 cs.FL math.GR
Automata Minimization: a Functorial Approach
在本文中，我们认为语言和它们的受体-如确定性或加权自动机，换能器，或monoid-作为函子从输入类别，指定的语言和机器的类型的类别，指定的输出类型。我们的结果如下：a）我们提供了关于输出范畴的充分条件，从而保证了相应自动机的最小化。b）我们展示了如何将输出值的类别之间的转换提升为自动机类别之间的转换。c）我们展示了这个框架如何应用于自动机理论中的几种现象，从确定性和最小化开始（以前从共代数和对偶理论的角度进行了研究）。我们特别适用于这些技术的Choffrut的最小化算法的连续传感器和重温Brzozowski的最小化算法。
2017-11-08 cs.FL
Combinatorial structures connecting Latin squares and bireversible automata
University of South Florida（南佛罗里达大学）
从组合视角探索字母变换器等自动机理论，将其转移集视为正交阵列类似物，讨论相关组合编码，用组合结构刻画各类自动机，提出字母变换器同构概念，推广对称性并保持双可逆自动机类别。
2026-07-29 cs.FL math.CO math.GR
Tree Automata as Algebras: Minimisation and Determinisation
我们研究了树自动机的范畴推广，作为$Σ$ -代数的固定endofunctor $Σ$赋予初始和最终状态。根据温和的假设下的基本类别，我们提出了一个一般的最小化算法，这些自动机。然后，我们建立和扩展现有的概括的Nerode等价到一个分类设置，并将其与最小自动机的存在。最后，我们表明，广义类型的副作用，如非决定论，可以捕捉到这个范畴的框架，导致一个一般的确定性程序。
2019-07-16 cs.FL
A Categorical Framework for Learning Generalised Tree Automata
自动机学习是一种流行的技术，用于从查询中自动构造自动机模型。许多研究都致力于为不同类型的自动机设计专门的算法适应性。CALF项目试图使用范畴理论来统一这些，以简化正确性证明并指导新算法的设计。在本文中，我们扩展CALF涵盖学习的代数结构，可能没有一个coalgebraic介绍。此外，我们提供了一个详细的算法帐户的抽象版本的流行的L * 算法，这是从CALF失踪。我们将抽象理论实例化到一大类集合函子上，从而第一次从抽象框架中恢复出实用的树自动机学习算法，同时获得了学习约束多项式函子代数的新算法.
2022-05-02 cs.FL
Implicit automata in typed $λ$-calculi II: streaming transducers vs categorical semantics
本文将正则字符串转换刻画为带加法算子的线性 λ-演算程序，通过编码无复制流式字符串转换器并利用范畴语义学建立等价关系，进而将结果推广至树结构并揭示其与线性逻辑的联系。
2021-08-25 cs.FL cs.LO
Efficient Automata-based Planning and Control under Spatio-Temporal Logic Specifications
时空逻辑在控制中的使用是出于对动态系统施加复杂的空间和时间行为并相应地控制这些系统的需要。合成正确的设计控制律是一项具有挑战性的任务，导致计算要求高的方法。我们认为有效的自动机为基础的规划连续时间系统下的信号间隔时序逻辑规范，表达片段的信号时序逻辑。规划是基于最近的结果，自动机为基础的验证度量区间时序逻辑。获得接受满足度量间隔时间逻辑规范的所有布尔信号的定时信号转换器，该度量间隔时间逻辑规范是从手头的信号间隔时间逻辑规范中提取的。该传感器被修改，以考虑信号间隔时间逻辑规范的空间特性，表征满足该规范的所有实值信号。使用基于逻辑的反馈控制法，如我们在早期的作品中提出的，然后，我们提供了一个抽象的系统，在一个合适的方式，与修改后的定时信号传感器对齐。这允许避免通常通过在系统的抽象和规范之间形成产品自动机而引起的状态空间爆炸。
2020-03-24 cs.FL
Expressiveness of Visibly Pushdown Transducers
可见下推传感器（VPT）是扩展了输出的可见下推自动机。它们已经被引入到嵌套单词的模型转换中，即具有调用/返回结构的单词。由于树和更一般的对冲可以线性化为（良好）嵌套的单词，VPT是一种自然的形式主义来表达在流中评估的树转换。本文的目的是精确地表征相对于其他树传感器模型的VPT的表达能力。
2013-11-21 cs.FL
Regular Expressions and Transducers over Alphabet-invariant and User-defined Labels
我们感兴趣的是正则表达式和转换器，它们以字母不变的方式表示单词关系-例如，所有单词对u，v的集合，其中v是u的前缀，与字母表无关。当前的形式语言对象的软件系统不具有定义这种对象的机制。我们定义转换器中的过渡标签涉及我们所谓的集规范，其中一些是字母不变的。事实上，我们给出了自动机类型对象的更广泛的定义，称为标记图，其中每个转换标签可以是任何字符串，只要该字符串表示某个幺半群的子集。然后，标记图的行为是该幺半群的子集。我们对正则表达式做同样的事情。我们获得了一些经典的算法构造普通正则表达式和换能器在广泛的水平上的标记图的扩展，并以这样的方式，扩展的结构的计算效率不牺牲。对于具有集合规范的正则表达式，我们得到了相应的偏导数自动机。对于设置规格的换能器，我们得到进一步的算法，可以应用于独立的正则语言的问题，特别是证人版本的独立属性满意度问题。
2018-05-04 cs.FL
On Functionality of Visibly Pushdown Transducers
可见下推换能器形成下推换能器的子类，其（严格地）扩展具有堆叠的有限状态换能器。就像下推自动机一样，输入符号决定堆栈操作。在本文中，我们证明了功能是可判定的PSpace的可见下推传感器。这个证明是通过一个pumping参数完成的：如果一个有两个输出的单词有足够大的嵌套深度，那么就存在一个有两个输出的嵌套单词，其嵌套深度严格地更小。证明中运用了词组合学的技巧。作为功能的可判定性的结果，我们还表明，等价的功能明显下推换能器Exptime完成。
2010-02-07 cs.FL
Transductions Computed by One-Dimensional Cellular Automata
元胞自动机的研究方向是它们计算转换的能力，即把输入转换成输出。所计算的转导的家庭被分类关于允许处理输入和计算输出的时间。由于对快速转换的兴趣特别浓厚，我们主要关注实时的和线性时间的时间复杂度。我们首先研究元胞自动机换能器的计算能力，通过比较它们的迭代阵列换能器，也就是说，我们比较并行输入/输出模式的顺序输入/输出模式的大规模并行机。通过直接模拟，证明了并行模式并不比顺序模式弱。此外，关于某些时间复杂度，元胞自动机换能器甚至比迭代阵列更强大。在本文的第二部分中，该模型的问题进行了比较的顺序设备单值有限状态传感器和确定性下推传感器。事实证明，这两种模型可以模拟元胞自动机换能器比迭代阵列换能器更快。
2012-08-14 cs.CC cs.DM cs.FL
Learning Weighted Automata over Number Rings, Concretely and Categorically
提出一种通用的主动学习归约过程，在数环加权自动机的具体设置中实现了多项式时间精确学习算法，并证明超越其状态数下界需依赖量子多项式时间的主理想问题求解。
2025-04-23 cs.FL
Towards an algebraic characterization of rational word functions
在形式语言理论中，几种不同的模型描述了正则语言，例如有限自动机、有限索引的同余或一元二阶逻辑（MSO）。此外，MSO的几个片段具有有效的特征的代数性质的基础上。当我们考虑转换器而不是自动机时，这样的刻画就更具挑战性了，因为正则语言的许多属性并不能推广到正则词函数。在本文中，我们考虑的字功能，是可定义的单向转换器（有理函数）。我们表明，典型的bimachine的Schutenauer和Schützenberger保留某些代数性质的有理函数，类似的情况下，文字语言。特别是，我们给出了一个有效的表征功能，可以定义一个非周期性的单向换能器。
2015-06-22 cs.FL
Freeness of automata groups vs boundary dynamics
我们证明了由丰富对偶变换器生成的（半）群的边界动力学表征了自动机群自由的代数性质。我们专门这个结果的类的双可逆换能器，我们表明，不自由的属性是等价的，有一个有限的Schreier图在边界上的丰富的对偶点上的一些基本上非平凡的点。从这些结果中，我们得到一些后果的动力学，算法和代数的观点。在本文的最后一部分，我们解决的问题，找到非双可逆换能器定义的自由群的例子，我们显示的例子，从每个国家的接收器产生自由群，并在一般情况下，我们链接到这个问题的不存在某些字有趣的组合和几何性质。
2014-11-03 cs.FL math.GR
Degrees of Infinite Words, Polynomials, and Atoms (Extended Version)
我们研究有限状态传感器和他们的权力转化为无限的话。符号的无限序列在从形式语言到纯数学和物理学的广泛领域中具有极其重要的意义。虽然用于识别和转换语言的有限自动机是众所周知的，但对自动机转换无限单词的能力知之甚少。有限状态传感器实现的字变换引起的复杂性比较的话，从而导致等价类，称为（换能器）度，和这些度的偏序。随后的层次结构类似于递归理论的不可解度，也称为图灵度，其中的转换设备是图灵机。然而，作为一个复杂性度量，图灵机太强大了：它们通过识别所有可计算的单词来简化分类问题。半导体状态传感器产生了一个更细粒度的，有区别的层次结构。与图灵度相反，几乎没有任何关于换能器度的信息，尽管它们是自然的。我们使用线性代数和分析的方法来证明，有无限多个原子的换能器度，也就是说，最小的非平凡度。
2018-03-08 cs.FL
What You Must Remember When Transforming Datawords
流数据字符串转换器（SDST）被引入来建模一类命令式程序和一类函数式程序，操纵数据项列表。这些可以用来编写常用的例程，如插入，删除和反转。SDST可以处理来自潜在无限数据域的数据值。流串转换器（SST）的模型是SDST的片段，其中无限的数据域被丢弃，只考虑有限的字母表。从语言理论的角度对SST进行了大量的研究。我们把数据引入到SST中，就像把数据引入到有限状态自动机中得到寄存器自动机一样。其结果是流串寄存器传感器（SSRT），这是SDST的子类。SDST可以在数据域上使用线性顺序比较数据值，这是SSRT无法完成的。我们给出了一个机器独立的SSRTs与起源语义的表征，沿着Myhill-Nerode定理。相似模型的独立于机器的特征描述已经形成了学习算法的基础，并使我们能够理解模型的片段。换能器的原点语义跟踪输出的哪些位置源自输入的哪些位置。虽然是一个限制，但使用原点语义是合理的，并且已知可以简化与换能器相关的许多问题。除了确定性寄存器自动机的特征之外，我们还使用起源语义作为技术构建块。然而，我们需要在这些基础上进行更多的建设，以克服SSRT特有的一些挑战。
2020-12-14 cs.FL
Deterministic pushdown automata can compress some normal sequences
本文构造了一个确定性下推转换器，成功压缩了一个正规数字序列，从而肯定解决了先前论文中遗留的开放问题。
2024-08-09 cs.FL
Pebble transducers with unary output
Bojaczyk最近开始了对确定性卵石换能器的深入研究，卵石换能器是一种双向自动机，可以在输入单词上留下标记（称为“卵石”），并产生输出单词。它们从一个词到另一个词描述功能。已经研究了该定义的两个自然限制：Douéneau-Tabot等人的大理石换能器，和比较自由卵石换能器（我们在这里重命名为“盲换能器”）的Nguyên等人。在这里，我们研究的可判定性的卵石，大理石和盲换能器，产生一元输出计算的函数类之间的隶属度问题。首先，我们表明，卵石和大理石换能器具有相同的表达能力时，输出是一元（这是假的非一元输出）。然后，我们描述了1卵石传感器与一元输出，描述了一个函数可计算的盲传感器，并表明，隶属度问题是可判定的。这些结果可以用程序的自动化简化来解释。
2022-09-30 cs.FL
Abstract Transducers
在过去的十年中，已经提出了几种对符号输入字母进行操作的抽象机器，例如符号自动机或格自动机。这些类型的自动机的应用包括软件安全分析和自然语言处理。虽然这些模型提供了在无限输入字母表上描述单词的方法，但在符号输出（如换能器中存在的）字母表或甚至其抽象（扩展）上没有相当大的工作。此外，已建立的用于转换（例如，最小化或减少）产生关于状态或转换的输出的有限状态机的方法不适用。这种类型的机器需要一个等价的概念来说明转换是否保持语义。我们提出了一种新形式的有限状态传感器的抽象传感器。它们的输入字母表和输出字母表都由抽象词组成，其中一个抽象词表示一组具体词。这些表征之间的映射由抽象词域描述。通过使用单词而不是单个字母，抽象转换器提供了lookaheads决定进行状态转换的可能性。由于每个转换上的输入符号和输出符号都是一个抽象实体，因此可以自然地应用抽象技术。我们应用抽象传感器的基础上共享任务工件重用的上下文中的程序分析和验证，并描述任务工件抽象的话。任务工件是对分析任务及其解决方案有贡献的任何实体，例如，候选不变量或要编织的源代码。
2019-10-16 cs.FL cs.PL
Synthesis of Data Word Transducers
本文研究数据ω-词上的反应式合成，针对扩展寄存器的自动机规范与转换器实现，探讨不同规范类型及寄存器有无界下的可判定性，提出通用技术并重新证明全称规范的有界合成可判定性。
2021-03-17 cs.FL
Unambiguous Forest Factorization
在本文中，我们看一个明确的版本西蒙的森林因子分解定理，一个非常深刻的结果，在代数，逻辑和自动机有广泛的联系。给定一个从$Σ^+$到有限半群$S$的态射$φ$，我们构造了一个对$φ$是“好的”的泛的无歧义自动机A. $\Aa$的优点为森林因子分解定理提供了一个非常简单的证明，为$Σ^{\infty}$中的任何单词提供了一个Ramsey分裂，使得Ramsey分裂的高度由A的状态数限制。从morphim $φ$合成良好自动机的一个重要应用是构造与确定性双向转换器相对应的正则转换器表达式（RTE）。
2018-10-03 cs.FL
String Solving with Stabilization and Transducers (Technical Report)
Faculty of Information Technology, Brno University of Technology（布尔诺理工大学信息技术学院）；The Technical Faculty of IT and Design, Aalborg University（奥尔堡大学IT与设计技术学院）
本文提出了一种基于自动机的高效方法，用于求解字符串约束，通过稳定化方法改进了Z3-Noodler求解器，以支持由有限状态转录机表示的关系约束。该方法通过减少昂贵的连接消除需求，提高了长度约束的处理效率，并提出了有效的启发式方法，显著提升了求解性能。
2026-05-18 cs.FL cs.LO
Complete Compositional Syntax for Finite Transducers on Finite and Bi-Infinite Words
本文提出以有限状态非确定性传感器统一自动机理论、迁移系统与sofic子移位，并给出带可靠改写规则的组合图解语法，证明其等式理论完全性。
2025-02-10 cs.DM cs.FL cs.LO
Slightly Non-Linear Higher-Order Tree Transducers
Aix-Marseille University（艾克斯-马赛大学）；CNRS（法国国家科学研究中心）；Université Paris Cité（巴黎西岱大学）
本文研究了略微非线性的高阶树转换器，证明其等价于不可见 Pebble树转换器，并探讨了仿射λ转换器与隐式自动机的关系。
2026-03-11 cs.FL cs.LO
The structure of polynomial growth for tree automata/transducers and MSO set queries
Universität Bremen（不来梅大学）；Aix-Marseille University（艾克斯-马赛大学）；CNRS（法国国家科学研究中心）
本文研究了树自动机/转换器的多项式增长结构及MSO集合查询，提出了多项式增长度数的决策方法，并探讨了相关树到树函数的增长率和子类成员问题。
2026-01-06 cs.FL cs.LO
Automata Minimization: a Functorial Approach
本文提出函子框架统一自动机最小化，给出输出范畴充分条件保证最小化，提升伴随关系，并解释Choffrut与Brzozowski算法。
2020-03-20 cs.FL cs.LO
Revisiting the Equivalence Problem for Finite Multitape Automata
确定性多带自动机（或转换器）的判定等价性是一个长期存在的开放问题，直到Harju和Karhumäki在20世纪90年代初解决。他们的可判定性证明产生了一个co_NP上界，但显然对问题的复杂性知之甚少。在本文中，我们给出了另一种证明的可判定性，它遵循的基本策略的Harju和Karhumaki，但取代他们使用群论的结果矩阵代数。从我们的证明，我们得到一个简单的随机算法，决定语言等价的确定性多带自动机，更一般地说，多重性等价的非确定性多带自动机。该算法只涉及矩阵求幂，并在多项式时间内运行每个固定数量的磁带。如果两个输入自动机是不等价的，那么算法输出一个它们不同的词。
2013-05-02 cs.FL
Continuous Speech Recognition Based on Deterministic Finite Automata Machine using Utterance and Pitch Verification
介绍了一套用于基于话语验证（UV）的连续语音识别（CSR）的声学建模技术。在这项工作中，话语验证意味着能够确定假设的单词串的部分何时对应于可能出现在话语中的错误解码的词汇表单词或词汇表外单词。这种能力在这里被实现为似然比（LR）。这里介绍了两种UV技术。首先是语音验证和词汇测试，同时根据与LR度量直接相关的优化准则生成UV模型的参数。第二种技术是基于加权有限状态传感器的基音识别。这些转换器为语音识别系统的主要组件提供了一种通用和自然的表示，这些组件包括隐马尔可夫模型（HMRM）、上下文相关模型、发音词典、统计语法以及单词或音素网格。有限状态机处理UV模型的声学参数。本文提出的实验研究结果表明，LR为基础的参数估计结果在一个显着改善UV性能为这项任务。该研究还发现，与现有的UV程序相比，使用基于LR的加权有限状态换能器以及UV可以提供高达11%的UV性能改善。最后，还发现有限状态机的性能高度依赖于在训练声学模型中使用LR准则。几个意见的文件中有关的UV和这些技术与统计语言模型的相互作用的信心措施的形成。
2014-01-21 cs.FL
A categorical framework for cellular automata
Centro Universitario de Ciencias Exactas e Ingenierías, Universidad de Guadalajara（瓜达拉哈拉大学精确科学与工程大学中心）
本文提出基于范畴论的细胞自动机广义框架，通过群同态扩展理论，统一了现有概念并提供基础结果的纯粹范畴证明。
2026-02-03 cs.FL math.CT math.DS
Primitive Recursive Presentations of Automata and their Products
讨论了通过原始递归函数抽象指定Moore型状态机（传感器）和通过同时原始递归定义并行组合的方法。该方法主要是作为一种简洁方便的方式来处理计算机编程和工程中发现的复杂状态系统，但有一小部分表明与代数自动机理论和Krohn和Rhodes定理的联系。
2010-01-10 cs.FL cs.LO
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
Edit Distance of Finite-Valued Transducers
Université libre de Bruxelles（布鲁塞尔自由大学）
研究有限值转换器的编辑距离计算问题，证明其可计算性，扩展了功能转换器的研究范围。
2026-05-07 cs.FL cs.LO
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
Glushkov's construction for functional subsequential transducers
Glushkov的结构有许多有趣的性质，当应用于换能器时，它们变得更加明显。本文致力于展示这种算法的可能扩展和优化的范围。介绍了正则表达式的特殊形式，它可以有效地转换为无$ε$的泛函序贯加权有限状态变换器。产生的自动机是非常紧凑的，因为它们只包含一个状态的每个符号（从输入字母表）的原始表达和只有一个过渡的每个范围的符号，无论有多大。这种紧凑化的转换范围允许在自动机评估期间进行有效的二进制搜索查找。本文提出的方法和算法已用于实现多带转换器正则表达式的开源编译器。
2020-09-22 cs.CL cs.FL
Church Synthesis on Register Automata over Linearly Ordered Data Domains
本文研究线性有序数据域上寄存器自动机规范的Church综合，提出单侧Church博弈并证明其可判定性（ExpTime），并应用于换能器综合。
2023-06-22 cs.FL
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
On Computability of Data Word Functions Defined by Transducers
在本文中，我们研究的问题，合成可计算函数的无限字在一个无限的字母表（数据欧米茄字）。可计算性的概念是通过具有无限输入的图灵机来定义的，它可以在极限下产生相应的无限输出。我们使用非确定性传感器配备寄存器，寄存器自动机的扩展与输出，指定功能。这样的换能器可能不定义功能，但更一般的关系的数据欧米茄字，我们表明，它是PSpace完整的测试是否一个给定的换能器定义了一个功能。然后，给定一个函数定义的一些寄存器转换器，我们表明，它是可判定的（再次，PSpace完全）是否这样的功能是可计算的。对于已知的有限字母表的情况下，我们表明，可计算性和连续性一致的功能定义的寄存器换能器，并显示如何确定连续性。我们还定义了一个子类，这些问题是可解的多项式时间。
2020-02-19 cs.FL cs.LO
Static Analysis of Communicating Processes using Symbolic Transducers
我们提出了一个通用模型，允许静态分析的基础上抽象的解释系统的通信过程。我们的技术受到常规模型检验的启发，将程序状态集表示为格自动机，将程序语义表示为符号转换器。该模型可以表示进程和通信的动态创建/销毁。使用抽象的解释框架，我们能够提供一个健全的过度近似的系统的可达集，从而使我们能够证明安全属性。我们在一个原型中实现了这种方法，该原型针对C程序的MPI库。
2016-11-27 cs.FL cs.LO cs.SE
Automata Learning: An Algebraic Approach
Friedrich-Alexander-Universität Erlangen-Nürnberg（埃尔朗根-纽伦堡大学）
我们提出了一个通用的分类框架学习未知的各种类型的形式语言（例如有限或无限的话，加权和名义语言）。我们的方法是参数的单子T，代表给定类型的语言和它们的识别代数结构。利用T-代数的anautomata表示的概念，我们证明了学习T-可识别语言的任务可以简化为学习代数自动机的抽象形式，其转换由函子建模。对于伴随自动机这一重要情形，我们设计了一个推广Angluin L* 的学习算法。该算法是措辞的分类描述的扩展步骤，我们提供了一个专用的概念有限的基础上的终止和复杂性分析。我们的框架适用于像欧米茄-正则语言这样的结构，这些结构不在自动机学习的现有分类帐户的范围内。此外，它产生了新的学习算法的几种类型的语言，没有这样的算法以前是已知的，包括排序语言，名义语言与名称绑定，成本函数。
2020-08-28 cs.FL cs.LG cs.LO
Implicit automata in λ-calculi III: affine planar string-to-string functions
本文通过非交换仿射逻辑的λ-项刻画一阶字符串转换，扩展星自由语言结果，利用Krohn-Rhodes分解和双向可逆平面换能器证明双向包含，并处理范畴单位非终对象的挑战。
2024-12-07 cs.FL cs.LO
Separating Words with Automata in the Half-adversarial Case
LaBRI, Université de Bordeaux（波尔多大学 LaBRI）
本文研究半对抗场景下的DFA单词区分问题，证明对均匀随机二进制单词u，高概率下可用状态数为$O(\n^{7/3} n \log n)$的DFA区分u与任意其他单词，核心方法是利用随机单词结构稀疏性，通过分块压缩将问题归约为短游程编码单词的区分。
2026-08-31 cs.FL
Synchronization of Deterministic Visibly Push-Down Automata
我们将有限自动机的同步字的概念推广到确定性的下推自动机，它将自动机的所有状态映射到同一个状态。这里，同步字w不仅将所有状态映射到相同的状态，而且在读取w之后满足关于每个运行的栈内容的某些条件。我们考虑三种类型的栈约束：在读取w后，栈（1）在每次运行中为空，（2）在每次运行中包含相同的栈符号序列，或（3）包含独立于其他运行的任意序列。我们证明了，与一般的确定性下推自动机相比，对于确定性可见下推自动机，是否存在具有这些堆栈约束的同步字是可判定的，即，问题出在EXPTIME上。在约束条件（1）下，该问题甚至在P中。对于确定性非常明显的下推自动机的子类，该问题对于所有三种类型的约束都在P中。我们进一步研究了同步问题的变体，其中由同步字引起的堆栈高度行为的匝数受到限制，以及同步顺序换能器的变体的问题，该变体显示出一些明显的行为，由一个字来描述状态并在所有运行中产生相同的输出。
2020-07-17 cs.CC cs.FL
On the Structure Theory of Partial Automaton Semigroups
我们研究自动机结构，即群，幺半群和半群产生的自动机，这在这种情况下，意味着一个确定性的有限状态字母到字母的转换器。而不是只考虑完全自动机，我们专门研究半群产生的部分自动机。首先，我们证明了部分自动机生成的半群类与完全自动机生成的半群类重合当且仅当后者在去除先前的伴随零下是闭的，这是Cain所述的（完全）自动机半群理论中的一个公开问题。然后，我们证明了，没有半直积（因此，也没有直积）的任意半群的（非平凡）子半群的自由单演半群是一个自动机半群。最后，我们集中讨论由可逆但部分自动机生成的逆半群，我们称之为自动机逆半群，并证明任何逆自动机半群都可以由这样的自动机生成（证明自动机逆半群和逆自动机半群重合）。
2020-07-16 cs.FL math.GR
Structural Complexity of Multi-Valued Partial Functions Computed by Nondeterministic Pushdown Automata
本文继续对CFL函数的结构性质进行了系统和全面的研究，CFL函数通常是由配备只写输出带（或下推转换器）的单向单头非确定下推自动机计算的多值部分函数，其中CFL指与上下文无关语言的相关性。CFL函数的行为往往与其相应的上下文无关语言完全不同。我们广泛地讨论了包含，分离，并通过应用布尔运算，功能组合，多-一相对化，图灵相对化从CFL功能得到的各种类别的功能之间的细化。特别是，图灵相对化有助于构建CFL函数类的层次结构。我们还分析了优化函数的计算复杂性，即寻找CFL函数的最优值，并讨论了它们与相关语言的关系。
2015-08-24 cs.CC cs.FL
Path category for free - Open morphisms from coalgebras with non-deterministic branching
对于过渡系统的变分及其互模拟有不同的分类方法。一类是函子G的余代数，其中互模拟定义为G-余代数同态的一个跨距。另一个是在路径范畴和开态射方面，其中互模拟被定义为开态射的跨度。这种相似性不是巧合：给定一个函子G，满足一定的条件，我们导出了点G-余代数和松弛同态的路范畴，使得开态射恰好是G-余代数同态。上述构造为不同类型的变迁系统免费提供了路径范畴和迹语义：（1）非确定性树自动机（2）正则非确定性名义自动机（RNA），一种生活在名义集合中的表达自动机概念（3）多分类变迁系统。这最后一个例子与拉索塔的结构有关，它是在相反的方向上。
2019-02-15 cs.FL
