CALF: Categorical Automata Learning Framework
自动机学习是一种已成功应用于验证的技术，自动机类型根据应用领域而变化。自动机学习算法的适应性越来越复杂的自动机类型必须从头开始开发，因为没有抽象的理论提供指导。这使得设计这样的算法变得困难，并且模糊了它们的正确性证明。我们介绍了一个简单的范畴理论的形式主义，提供了一个适当的抽象的基础，研究自动机学习。此外，我们的框架建立了学习，测试和最小化算法之间的正式关系。我们说明了它的一般性与两个例子：确定性和加权自动机。
2017-06-26 cs.FL
Towards Nominal Formal Languages
我们介绍了形式语言在无限的字母表中的话可能包含粘合剂。我们定义了名义语言、名义幺半群和名义正则表达式的概念。此外，我们通过增加栈来扩展历史依赖自动机（HD-自动机），并研究了名义语言的可识别性。
2011-02-16 cs.FL
Standard Automata Theory and Process Algebra
本文探讨了经典自动机理论在现代系统规范与验证中的应用，包括并发系统，回顾了早期对自动机理论的批评并提供了历史文献综述。
2026-04-19 cs.FL
Nominal Automata with Name Deallocation
Friedrich-Alexander-Universitt Erlangen-Nrnberg（弗里德里希·亚历山大埃尔朗根-纽伦堡大学）
本文提出一种新的命名自动机模型，用于描述具有显式分配和释放的数据词语言，通过添加释放转换扩展了现有模型，并证明其与自然表达语言的等价性。
2026-03-25 cs.FL
NeuroSTAR: Automata-guided Neuro-symbolic Specification Formalization
University of Virginia（弗吉尼亚大学）；William & Mary（威廉玛丽学院）
本研究提出NeuroSTAR框架，通过多生成器获取LTLf候选并基于DFA迹优化，在NL转LTLf任务上性能提升8-18个百分点，在驾驶法规文本中83.9%的段落可捕捉必要时序语义，验证了其有效性。
2026-09-04 cs.FL
Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第六届国际游戏、自动机、逻辑和形式化验证研讨会（GandALF 2015）的会议记录。研讨会于2015年9月21日和22日在意大利热那亚举行。专题讨论会的会议记录载有三次应邀演讲的摘要和13篇论文，这些论文是经过仔细评估后被接受在会议上介绍的。被接受的论文的主题包括算法博弈论，自动机理论，形式化验证，模态和时序逻辑。
2015-09-23 cs.FL cs.LO
On the Use of Quasiorders in Formal Language Theory
在这篇论文中，我们使用词的拟序提供了一个新的视角，从形式语言理论的两个研究得很好的问题：确定语言包含和操纵有限自动机表示的正则语言。首先，我们提出了一个通用的准序为基础的框架，当实例化与不同的准序，产生不同的算法（其中一些新的）决定语言的包容性。然后，我们实例化这个框架，设计一个高效的算法搜索与正则表达式的语法压缩文本。最后，我们定义了一个基于准序的自动机构造框架，为剩余自动机提供了一个新的视角。
2020-08-20 cs.FL
On Quotients of Formal Power Series
商是形式语言的一种基本运算，在构造最小确定有限自动机和泛自动机中起着关键作用。本文将该运算推广到形式幂级数，并系统地研究了它在加权自动机研究中的应用。特别是，我们定义了两个商操作的正式幂级数，符合计算时，由一个字。我们将第一个操作称为（左或右）\emph{quotient}，将第二个操作称为（左或右）\emph{residual}。为了支持余元和剩余的定义，底层半环被限制为完全半环或完全c-半环。在形式幂级数的情况下，得到了类似于经典情况的代数性质。此外，我们还证明了正则级数和加权上下文无关级数的闭包性质，在幂次项和残差项下，与形式语言中的闭包性质相似。使用这些操作，我们为每个形式幂级数$A$定义两个加权自动机${\cal M}_A$和${\cal U}_A$。这两个加权自动机都接受$A$，而${\cal M}_A$是$A$的最小确定性加权自动机。${\cal U}_A$的普遍性是合理的，特别是，我们表明，${\cal M}_A$是一个子自动机的${\cal U}_A$。最后，本文给出了构造泛自动机的一种有效方法。
2012-03-10 cs.FL
Frequency Automata: A novel formal model of hybrid systems in combined time and frequency domains
本文首次提出结合时域和频域的混合系统形式化模型——频域自动机，通过从混合自动机的可靠转换及数值仿真器，实现了精确电平交叉检测，仿真速度较Simulink/Stateflow提升118至1129倍。
2025-05-30 cs.FL
Proceedings Seventeenth International Symposium on Games, Automata, Logics, and Formal Verification
本文是关于GandALF 2026研讨会论文集的介绍，该会议于2026年在丹麦奥尔堡举行，旨在汇集博弈、自动机、逻辑与形式化验证领域的研究者，促进理论与应用的交叉融合。
2026-10-08 cs.FL cs.LO
Proceedings 12th International Symposium on Games, Automata, Logics, and Formal Verification
本卷包含第12届国际游戏，自动机，逻辑和形式化验证研讨会（GandALF 2021）的会议记录。Gandalf 2021研讨会的目的是汇集来自学术界和工业界的研究人员，他们积极参与游戏，自动机，逻辑和形式化验证领域的工作。其想法是涵盖从理论到应用的广泛主题，并促进相互交流。
2021-09-16 cs.FL cs.GT cs.LO
Formalizing Time4sys using parametric timed automata
关键的实时系统必须经过验证，以避免在出现故障时造成严重后果的风险。泰利斯开发了一个开放的形式主义Time4sys模型实时系统，具有表达功能，如周期性或零星的任务，任务依赖性，分布式系统等，但是，Time4sys不允许原生的正式推理。在这项工作中，我们提出了一个翻译从Time4sys（参数）时间自动机，以便允许一个形式化验证。
2019-05-23 cs.FL cs.SE
Proceedings of the 13th International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第13届国际游戏，自动机，逻辑和形式化验证研讨会（GandALF 2022）的会议记录。Gandalf 2022研讨会的目的是汇集来自学术界和工业界的研究人员，他们积极参与游戏，自动机，逻辑和形式化验证领域的工作。其想法是涵盖从理论到应用的广泛主题，并促进相互交流。
2022-09-19 cs.FL cs.GT cs.LO
Proceedings 17th International Conference on Automata and Formal Languages
该论文集收录了AFL 2026的3篇特邀报告及18篇录用论文，这些论文来自14国作者，覆盖自动机与形式语言理论及其多领域应用。
2026-08-25 cs.CC cs.FL
Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification
本卷包含第九届游戏，自动机，逻辑和形式化验证国际研讨会（GandALF 2018）的会议记录。研讨会于2018年9月26日至28日在德国萨尔布吕肯举行。Gandalf研讨会是由一群意大利计算机科学家建立的，他们对数学逻辑、自动机理论、博弈论及其在复杂系统规范、设计和验证中的应用感兴趣。它的目的是提供一个论坛，让来自不同地区，可能有不同背景的人可以进行富有成效的互动。Gandalf具有真正的国际精神，这一点可以从项目和指导委员会的组成以及提交论文的国家分布中得到证明。
2018-09-07 cs.FL cs.LO
Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第七届国际游戏、自动机、逻辑和形式化验证研讨会（GandALF 2016）的会议记录。研讨会于2016年9月14日至16日在意大利卡塔尼亚举行。研讨会的会议记录包括3个特邀演讲的摘要和21篇论文全文，这些论文是经过仔细评估后被接受在会议上发表的。被接受的论文的主题涵盖算法博弈论，自动机理论，综合，形式化验证，动态，模态和时态逻辑。
2016-09-13 cs.FL cs.GT cs.LO
Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing
Formal Methods and Tools Lab, ISTI–CNR, Pisa, Italy（ISTI-国家研究委员会，意大利比萨）
本文基于Uppaal对合同自动机运行环境进行形式化建模、验证与测试，以提升开源分布式应用的可靠性。
2026-03-04 cs.FL cs.SE
Proceedings of the Fourteenth International Symposium on Games, Automata, Logics, and Formal Verification
该论文集汇集GandALF 2023关于博弈、自动机、逻辑与形式验证的研究，旨在连接学界与业界并推动理论及应用的交叉融合。
2023-09-29 cs.CC cs.FL cs.LO
Greibach Normal Form for $ω$-Algebraic Systems and Weighted Simple $ω$-Pushdown Automata
在加权自动机理论中，许多关于形式语言的经典结果被推广到定量的环境中。在这里，我们研究加权上下文无关语言的无限词，一个推广的$ω$ -上下文无关语言（科恩，黄金1977年）和扩展的加权上下文无关语言的有限词（乔姆斯基，Schützenberger 1963年）。在形式文法的理论中，这些加权上下文无关语言，或$ω$ -代数级数，可以表示为混合$ω$ -代数方程组的解和加权$ω$ -下推自动机。在我们的第一个主要结果中，我们证明了（混合）$ω$ -代数系统可以转化为Greibach范式。我们在第二个主要结果中使用Greibach范式证明了简单的$ω$ -复位下推自动机识别所有的$ω$ -代数级数。简单的$ω$ -复位自动机不使用$ε$ -转换，最多只能改变一个符号的堆栈。这些结果将上下文无关语言的基本性质推广到加权上下文无关语言。
2021-10-05 cs.FL
Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第五届国际游戏、自动机、逻辑和形式化验证研讨会（GandALF 2014）的会议记录。研讨会于2014年9月10日至12日在意大利维罗纳举行。专题讨论会的会议记录载有三次应邀演讲的摘要和19篇论文，这些论文是经过仔细评估后被接受在会议上发表的。被接受的论文的主题范围很广，包括算法和行为博弈论，博弈语义学，形式语言和自动机理论，模态和时序逻辑，软件验证，混合系统。
2014-08-24 cs.FL cs.GT cs.LO
Proceedings Fourth International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第四届国际游戏、自动机、逻辑和形式化验证研讨会（GandALF 2013）的会议记录。研讨会于2013年8月29日至31日在意大利Borca di Cadore举行。专题讨论会的会议记录载有三次应邀演讲的摘要和17篇论文，这些论文是经过仔细评估后被接受在会议上发表的。被接受的论文的主题范围很广，包括算法和行为博弈论，博弈语义学，形式语言和自动机理论，模态和时序逻辑，软件验证，混合系统。
2013-07-16 cs.FL cs.GT cs.LO
Weighted Automata and Regular Expressions for Financial Systems
Institut für Informatik, Universität Leipzig（莱比锡大学）
本文引入加权有限金融自动机（WFFA）作为建模和分析金融系统定量属性的框架，通过股票价格、利率等不确定经济变量驱动。提出加权金融正则表达式用于描述定量金融属性，并建立WFFA与正则表达式之间的Kleene-Schützenberger型对应关系，研究WFFA的基本决策和优化问题。
2026-04-19 cs.FL
Proceedings Fifteenth International Symposium on Games, Automata, Logics, and Formal Verification
本卷是2024年6月在冰岛雷克雅未克举办的第十五届GandALF研讨会论文集，该会汇聚游戏、自动机等领域产学研研究者，覆盖理论到应用主题以促进跨领域融合。
2024-10-29 cs.CC cs.FL cs.LO
Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification
本卷包含第11届游戏，自动机，逻辑和形式化验证国际研讨会（GandALF 2020）的会议记录。研讨会于2020年9月21日至22日以完全在线的方式举行。Gandalf研讨会是由一群意大利计算机科学家建立的，他们对数学逻辑、自动机理论、博弈论及其在复杂系统规范、设计和验证中的应用感兴趣。它的目的是提供一个论坛，让来自不同地区，可能有不同背景的人可以进行富有成效的互动。Gandalf具有真正的国际精神，这一点可以从项目和指导委员会的组成以及提交论文的国家分布中得到证明。
2020-09-20 cs.FL cs.GT cs.LO
Proceedings Tenth International Symposium on Games, Automata, Logics, and Formal Verification
本卷包含第十届游戏，自动机，逻辑和形式化验证国际研讨会（GandALF 2019）的会议记录。研讨会于2010年9月2日至3日在法国波尔多举行。Gandalf研讨会是由一群意大利计算机科学家建立的，他们对数学逻辑、自动机理论、博弈论及其在复杂系统规范、设计和验证中的应用感兴趣。它的目的是提供一个论坛，让来自不同地区，可能有不同背景的人可以进行富有成效的互动。Gandalf具有真正的国际精神，这一点可以从项目和指导委员会的组成以及提交论文的国家分布中得到证明。
2019-09-12 cs.FL cs.GT cs.LO
Proceedings Eighth International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第八届游戏、自动机、逻辑和形式化验证国际研讨会（GandALF 2017）的会议记录。研讨会于2017年9月20日至22日在意大利罗马举行。Gandalf研讨会是由一群意大利计算机科学家建立的，他们对数学逻辑、自动机理论、博弈论及其在复杂系统规范、设计和验证中的应用感兴趣。它的目的是提供一个论坛，让来自不同地区，可能有不同背景的人可以进行富有成效的互动。Gandalf具有真正的国际精神，这一点可以从项目和指导委员会的组成以及提交论文的国家分布中得到证明。
2017-09-06 cs.FL cs.GT cs.LO
Dual Adjunction Between $Ω$-Automata and Wilke Algebra Quotients
本文引入lasso半群推广Wilke代数，证明有限lasso半群刻画正则lasso语言，并建立lasso自动机与自由lasso半群商之间的对偶伴随，进而将其限制到$Ω$-自动机与自由Wilke代数商之间。
2024-11-22 cs.FL
Proceedings First Symposium on Games, Automata, Logic, and Formal Verification
本卷包含了第一次研讨会上的“游戏，自动机，逻辑，和形式化验证（GandALF）"，在米诺里（阿马尔菲海岸），意大利，2010年6月17日至18日举行的会议记录。研讨会由一些对博弈论、数理逻辑、自动机理论及其在复杂系统的规范、设计和验证中的应用感兴趣的意大利计算机科学家推动。它涵盖了大量的研究课题，从理论方面到具体应用。它的目的是提供一个论坛，让来自不同地区的人，可能有不同的背景，可以成功地互动。该活动的高水平国际形象由节目委员会的组成和最终节目见证。
2010-06-09 cs.FL cs.GT cs.LO
Dynamic Input/Output Automata: a Formal and Compositional Model for Dynamic Systems
我们提出了动态I/O自动机（DIOA），动态系统的组合模型。在DIOA中，随着计算的进行，自动机可以动态地创建和销毁，并且自动机可以动态地改变其签名，即，它可以参与的一系列行动。DIOA具有用于并行组合、操作隐藏、操作重命名的操作符、自动机创建的概念以及通过跟踪包含的行为子类型的概念。DIOA可以使用签名修改来建模移动性，并且是分层的：一个动态变化的交互自动机系统本身被建模为单个自动机。我们还表明，并行组成，行动隐藏，行动重命名，和（受一些技术条件）自动机的创建都是单调的轨迹包含：如果一个组件被替换为另一个的痕迹是前者的一个子集，那么作为一个整体的系统的痕迹集只能减少。
2016-04-20 cs.DC cs.FL
Some Subclasses of Linear Languages based on Nondeterministic Linear Automata
在本文中，我们考虑类的非确定线性自动机作为一个模型的线性语言类。像其他自动机模型一样，自动移动不会增加接受能力。本文的主要贡献是引入了确定性线性自动机和偶线性自动机，即非确定性线性自动机分别对确定性语言类和偶线性语言类的自然限制。特别是，对于“确定性”线性语言的类别，有不同但不等同的建议。我们在这里证明了确定性线性自动机所接受的语言类不包含在这些类中的任何一个中，事实上它们正确地包含这些类。另一个贡献是生成了一个无限层次的形式语言，从确定性线性自动机接受的语言类，并在极限下实现了线性语言类。
2016-11-30 cs.FL
Hybrid Automata for Formal Modeling and Verification of Cyber-Physical Systems
离散控制（“网络”）和模拟环境（“物理”）之间的紧密集成-通过有线或无线通信网络上的传感器和执行器-是网络物理系统的定义特征。因此，信息物理系统的功能正确性不仅关键地取决于模拟物理环境的动态，而且还取决于改变环境动态的离散控制所采取的决策。混合自动机的框架-介绍了由Alberr，Courcoubetis，Henzinger和Ho-提供了一个正式的建模和规范环境来分析网络物理系统的离散和连续部分之间的相互作用。混合自动机可以被认为是有限状态自动机的推广，其在每个状态下的动态由常微分方程系统控制。此外，混合自动机的离散转换是由这些实值变量的值的约束，并使这些变量的演化不连续的跳跃。考虑到混合自动机中动力学的丰富性，一般模型的基本验证问题（如可达性和可扩展性）是不可判定的，这也许并不奇怪。在这篇文章中，我们提出了一个审查的混合自动机作为建模和验证框架的网络物理系统，并调查一些关键结果有关的实际验证问题的混合自动机。
2015-03-17 cs.FL cs.LO
From Transformers to Weighted Automata: Towards the Verification of Large Language Models
Ashoka University（阿育王大学）
本工作建立了Transformer与加权自动机之间的形式化桥梁，并提出恒等性测试算法，为严格验证大语言模型行为提供了首个理论框架。
2026-10-06 cs.FL cs.LG
Representing Formal Languages: A Comparison Between Finite Automata and Recurrent Neural Networks
Rice University（莱斯大学）；Baylor College of Medicine（贝勒医学院）
我们研究了递归神经网络（RNN）在学习识别规则形式语言时使用的内部表示。具体来说，我们在正则语言的正例和反例上训练RNN，并询问是否存在一个简单的解码函数，将该RNN的状态映射到该语言的最小确定性有限自动机（MDFA）的状态。我们的实验表明，这样的解码功能确实存在，它映射的状态的RNN不MDFA状态，但状态的{ \em抽象}通过聚类小集MDFA状态到“超状态”。定性分析表明，抽象往往有一个简单的解释。总的来说，结果表明RNN和有限自动机使用的内部表示之间存在很强的结构关系，并解释了RNN识别正式语法结构的众所周知的能力。
2019-02-27 cs.FL cs.LG
Precedence Automata and Languages
操作符先后次序语法定义了一个经典的布尔和确定性上下文无关族（称为Floyd语言或FL）。FL已经被证明严格包括众所周知的可见下推语言，并享受同样好的闭包属性。我们在这里介绍弗洛伊德自动机，一个等价的操作形式主义定义FL。这也允许扩展类来处理无限字符串，以执行例如模型检验。
2011-11-30 cs.FL
Towards a Digital Highway Code using Formal Modelling and Verification of Timed Automata
设计安全、可靠和值得信赖的自动驾驶汽车（AV）的挑战之一是确保AV遵守交通规则。为此，自动驾驶汽车需要能够理解和推理交通规则。在以前的工作中，我们引入了空间交通逻辑USL-TR，允许明确的，机器可读的，形式化的交通规则。这只是迈向可验证地遵守交通规则的自主交通代理的第一步。在本研究预览中，我们重点关注两个进一步的步骤：a）直接从交通规则中检索行为图，b）将行为图转换为使用USL-TR公式的时间自动机。有了这个，我们就有了一个正式的交通规则代表，并可以朝着建立数字公路代码的方向迈进。我们简要地设想进一步的步骤，其中包括添加环境和代理模型的时间自动机，最终实现和验证这些交通规则模型使用选择的形式化验证工具。
2022-09-28 cs.FL cs.LO cs.SE
Eve-positional languages: putting order into Büchi automata
Université Paris Cité, CNRS, IRIF（巴黎西岱大学、法国国家科学研究中心、IRIF研究所）
本研究提出一种基于受限非确定性Büchi自动机的新形式体系，刻画Eve位置ω-正则语言，补全既有研究的缺失结论，给出阶乘级规模膨胀的确定化方法，并证明其状态最优性。
2026-04-24 cs.FL
Track objects in cubical presheaf automata
University of Sheffield（谢菲尔德大学）；School of Computer Science（计算机学院）；University of Warsaw（华沙大学）；Institute of Mathematics（数学研究所）
该研究利用预层自动机形式体系，引入扩展高维自动机的新型并发建模自动机类，研究其语言并以正合余跨刻画。
2026-10-14 cs.FL math.CT
Functional Automata - Formal Languages for Computer Science Students
介绍性形式语言课程暴露了先进的本科生和早期研究生的自动机理论，语法，建设性的证明，可计算性和可判定性。编程专业的学生发现这些主题很有挑战性，或者在许多情况下，是压倒性的，并且处于计算机科学的边缘。这种看法的存在并不完全荒谬，因为学生被要求设计和证明正确的机器和语法，而不能进行实验，也不能得到即时反馈，这在学习环境中是必不可少的。这篇文章提出了计算理论应该使用实际构建计算的工具来教授的论点。它描述了一个库，FSM，旨在为学生提供实验和测试他们的设计使用状态机，语法和正则表达式的机会，实现和课堂使用。学生能够在进行正式的正确性证明之前进行随机测试。也就是说，学生可以像在编程课程中一样测试他们的设计。此外，图书馆很容易让学生实现他们开发的算法，作为他们编写的建设性证明的一部分。为学生提供这种能力应该是形式语言课堂的新趋势。
2014-12-16 cs.CY cs.FL
On Series-Parallel Pomset Languages: Rationality, Context-Freeness and Automata
并发Kleene代数（CKA）是研究并发程序的一种形式化方法.像以前的Kleene代数扩展一样，开发指称和操作视角之间的对应关系对于基础和应用都很重要。本文采取了重要的一步，这样的对应关系，通过精确的双Kleene代数（BKA），CKA的一个片段，一种新型的自动机，pomset自动机（PAs）。我们表明，PA可以实现BKA语义的串并行的理性表达式，一类PA可以被翻译回这些表达式。我们还讨论了一般PA的上下文无关的pomset文法的行为，因此，普遍性，等价性和串并行合理性的一般PA是不可判定的。
2018-12-14 cs.FL
Robust Biomolecular Finite Automata
我们提出了一个统一的方法，将任意的非确定性有限自动机（NFA）转换成一个确定性的质量作用输入/输出化学反应网络（I/O CRN），模拟它。I/O CRN接收其输入作为一个连续的时间信号组成的化学物种的浓度变化，以代表NFA的输入字符串在一个自然的方式。I/O CRN利用化学动力学的固有并行性，用NFA大小呈线性的许多化学物质实时的模拟NFA。我们证明了模拟是正确的，它是鲁棒的输入信号的扰动，物种的初始浓度，输出（决定），和I/O CRN的反应的速率常数。
2018-12-26 cs.CC cs.ET cs.FL
Quantitative Corner Case Feature Analysis of Hybrid Automata with ForFET$^{SMT}$
混合自动机（HA）模型的分析和验证是一项具有挑战性的任务。现有的方法和工具主要可以推理给定的属性是否被满足或违反。然而，这样的定性答案可能无法提供关于模型行为的足够信息。本文介绍了ForFET的$^{SMT}$工具，它可以用来定量地推理这些属性。它采用特征自动机，可以评估定量属性角的HA。ForFET $^{SMT}$使用两个第三方形式化验证工具作为其主干：SpaceEx可达性工具和SMT求解器dReach/dReal。在这里，我们描述了ForFET $^{SMT}$的设计和实现，并介绍了其功能和模块。为了提高非专业用户的工具的可用性，我们还提供了一个定量属性模板列表。
2020-12-30 cs.FL cs.LO
A Runtime Environment for Contract Automata
合同自动机已被引入指定的应用程序，通过行为合同和合成他们的编排作为有限状态自动机。本文讨论了合同自动机规范的应用程序的实现。我们提出了关怀，一个新的运行时环境，以协调服务实现合同，保证遵守其合同的实现。我们讨论如何照顾可以通过实现基于合同的应用程序，其正式的保证，我们确定所涉及的业务参与者的责任。实验显示了采用CARE相对于手动实现的好处。
2023-03-15 cs.FL cs.SE
A formal query language and automata model for aggregation in complex event recognition
University of Lille（里尔大学）
本文提出了一种扩展复杂事件逻辑（CEL）以支持聚合操作的查询语言ACEL，并引入了新的自动机模型ACEA，展示了其在复杂事件识别中的应用和表达力。
2026-01-02 cs.DB cs.FL cs.LO
Automata-based constraints for language model decoding
Google DeepMind（谷歌DeepMind）
针对语言模型难以保证生成形式语言有效字符串的问题，本文用自动机理论重构解码约束，为正则语言和确定性上下文无关语言给出高效闭式解，实现约7,000倍加速、可证明正确性与模块化扩展。
2024-08-05 cs.CL cs.FL
Automata Extraction from Transformers
Peking University（北京大学）
本文提出一种面向Transformer的自动机提取算法，通过跟踪其内部潜在表示变换并用L*算法将其解释为DFA，揭示了Transformer处理形式语言的机制，提升了模型可解释性。
2024-06-08 cs.AI cs.CL cs.FL
On Learning Nominal Automata with Binders
University of Leicester（莱斯特大学）；Gran Sasso Science Institute（格兰萨索科学研究所）
我们研究了一个学习算法的名义自动机的背景下，一个经典的自动机的字母特征的名称。这类自动机捕获了名义正则语言;类似于经典语言理论，名义自动机已经被证明可以用绑定器来替换名义正则表达式。这些形式主义是服从抽象建模资源感知计算。本文提出了一种带绑定器的标称正则语言的学习算法。我们的算法推广了Angluin的L* 算法，相对于名义正则语言与绑定器。我们证明了算法的正确性，并研究了算法的理论复杂度。
2019-09-12 cs.FL cs.LG
On the Linguistic Capacity of Real-Time Counter Automata
Allen Institute for AI（艾伦人工智能研究所）
计数器机器与自然语言处理（NLP）领域有了新的关联：最近的研究表明，一些性能强大的递归神经网络利用它们的记忆作为计数器。因此，理解这些网络成功的一个潜在方法是重新审视计数器计算理论。因此，我们研究了实时的【形】计数器机器作为形式语法的能力，重点是与NLP模型相关的形式属性。我们首先表明，几个变种的计数器机收敛表示同一类的形式语言。我们还证明了计数器语言在补，并，交和许多其他常见的集合运算下是封闭的。接下来，我们证明计数器机器不能评估布尔表达式，即使它们可以弱验证它们的语法。这对神经网络系统的可解释性和评估有影响：成功匹配语法模式并不能保证计数器记忆准确地编码组合语义。最后，我们考虑计数器语言是否是半线性的。这项工作的一般贡献的形式语言的理论是潜在的兴趣，了解循环神经网络。
2021-09-09 cs.CL cs.FL
Presheaf automata
本文提出预层自动机作为高维自动机等形式化方法的推广，发展了其语言理论基础并定义开映射扩展模拟与互模拟，证明了有限型预层自动机包含所有 Petri 网，且存在不满足 Kleene 定理的子类。
2025-08-15 cs.FL math.CT
A Formal Framework for the Explanation of Finite Automata Decisions
Department of Data Science and AI, Faculty of IT（数据科学与人工智能系，信息技术学院）
本文提出一种高效方法，用于确定有限自动机在特定输入词上的最小解释，以解释其行为并展示输入特征对结果的责任。
2026-02-17 cs.AI cs.FL cs.LO
From Automata Learning to Model Checking: Formal Security Verification of Black-Box Protocols
Mälardalen University（马尔默达尔大学）；AVL List GmbH（AVL李斯特有限公司）；AIT Austrian Institute of Technology GmbH（奥地利技术研究所有限公司）；KTH Royal Institute of Technology（皇家理工学院）
本文提出结合自动机学习与模型检查的方法，用于系统验证通信协议的安全属性，通过自动化流程减少建模工作量并提高安全性验证的自动化水平。
2026-09-14 cs.CR cs.FL
Incremental Monoidal Grammars
University of Oxford（牛津大学）；UCL（伦敦大学学院）
在这项工作中，我们定义形式文法的自由monoidal类别，以及一个函子从类别的形式文法的自动机。推广从布尔到任意半环，我们扩展我们的建设加权形式文法和加权自动机。这使我们能够将自然语言的分类观点与概率语言模型的标准机器学习概念联系起来。
2020-01-10 cs.AI cs.FL cs.LO
Weakly-unambiguous Parikh automata and their link to holonomic series
Inria and Université Paris-Saclay（法国国家信息与自动化研究所与巴黎萨克雷大学）；LIGM, Univ Gustave Eiffel, CNRS（拉格朗日计算机科学与应用实验室，巴黎东大学，法国国家科学研究中心）
本文研究了弱无歧义帕里克自动机与全息级数的关系，证明了其等价性并展示了生成级数的全息性质，同时探讨了包含问题的可判定性及复杂度上界。
2025-12-10 cs.FL cs.SC
Representing Hybrid Automata by Action Language Modulo Theories
Arizona State University（亚利桑那州立大学）；Houzz Inc.（Houzz 公司）
混合自动机和动作语言都是描述动态系统演化的形式化方法。本文建立了它们之间的正式关系。我们展示了如何简洁地表示混合自动机的动作语言，这反过来又被定义为一个高层次的符号的答案集编程模理论（ASPMT）-一个扩展的答案集程序的一阶水平类似的方式可满足性模理论（SMT）扩展命题可满足性（SAT）。首先，我们展示了如何表示线性混合自动机的凸不变量的行为语言模理论。进一步翻译成SMT允许使用支持实数运算的SMT求解器来计算它们。接下来，我们将表示扩展到一般类的非线性混合自动机，甚至允许非凸不变量。我们表示它们的动作语言模ODE（常微分方程），它可以被编译成可满足模ODE。我们开发了一个原型系统cplus 2aspmt的基础上，这些翻译，它允许一个简洁的表示的混合过渡系统，可以有效地计算的最先进的SMT求解器dReal。
2017-07-25 cs.AI cs.FL cs.LO
Automata Equipped with Auxiliary Data Structures and Regular Realizability Problems
我们考虑一般的计算模型：单向和双向有限自动机，对数空间图灵机，都配备了一个辅助数据结构（ADS）。ADS的定义基于ADS工作协议的语言。我们描述了连接的自动机为基础的模型与“气球自动机”，这是另一个一般的形式化的自动机配备了ADS Hopcroft和Ullman在1967年提出的。这个定义建立了ADS单向自动机的非空性问题、可由配备相同ADS的非确定性对数空间图灵机识别的语言和ADS协议语言的正则可实现性问题（NRR）之间的联系。NRR问题是验证输入上的正则语言是否与协议语言有非空交集。这些问题（和语言）的计算复杂性与对数空间约简是相同的。
2022-10-08 cs.CC cs.FL
