A Unifying Approach to Picture Automata
University of Bremen(不来梅大学);Charles University(查理大学)
提出使用有向无环图自动机识别图片语言,通过编码二维输入为DAG,并分析不同编码方式所对应的语言类。
2025-09-15 cs.FL
New Results on Vector and Homing Vector Automata
通过对向量自动机和归巢向量自动机的研究,我们给出了有限自动机的几个新的结果和各种扩张之间的联系。我们表明,归巢向量自动机优于扩展有限自动机时,都定义在$ 2 \times 2 $整数矩阵。我们研究了向量自动机的字符串分离问题,证明了具有有理项的广义有限自动机可以仅使用两个状态来分离任何一对字符串。研究了无状态归巢向量自动机,证明了一种语言可以被无状态盲确定性的带乘法的有限自动机实时版本识别当且仅当它是可交换的,并且它的Parikh像是线性齐次丢番图方程组的非负整数解的集合.
2019-05-28 cs.FL
Mata, a Fast and Simple Finite Automata Library (Technical Report)
本文介绍了一个用 C++ 编写的快速且简单的有限自动机库 Mata,它实现了模拟归约和反链语言包含检查等算法,提供 C++ 和 Python 接口,并在大规模基准上显著快于其他自动机库,同时支撑了高性能字符串求解器 Z3-Noodler。
2024-03-27 cs.FL
Reachability Analysis of Reversal-bounded Automata on Series-Parallel Graphs
字符串上的有限状态自动机的扩展,如多头自动机或多计数器自动机,已成功地用于编码许多无限状态非正则验证问题。在本文中,我们考虑一个推广的自动机理论的无限状态验证从字符串标记串并行图。我们定义了一个模型的非确定性,2路,并发自动机工作串并行图和通信通过共享寄存器的节点上的图形。我们考虑以下验证问题:给定一个系列的串并行图描述的上下文无关的图转换系统(GTS),并在串并行图的并发自动机,是一些图所产生的GTS接受的自动机?一般的问题是不可判定的已经(单向)多头自动机字符串。我们表明,一个有界的版本,其中自动机使固定数量的反转沿图,并使用固定数量的共享寄存器是可判定的,即使有没有约束的GTS生成的串并行图的大小。我们的可判定性结果是基于建立上下文切换的数量是有界的,并对有界并发自动机的计算进行编码,以将空性问题减少到下推自动机的空性问题。
2015-09-24 cs.FL
Constant-delay enumeration for SLP-compressed documents
本研究提出一种算法,在SLP压缩文档上,通过带注释自动机查询,实现预处理后恒定延迟枚举结果,改进了先前工作的对数延迟,并支持文档编辑。
2025-02-20 cs.DS cs.FL cs.LO
Finite Automata for Efficient Graph Recognition
本文在超边替换图文法框架下,将有限自动机从字符串提升到图,通过修改的幂集构造实现确定性化,并给出无需回溯识别图的充分条件。
2025-03-26 cs.FL
Enumeration on Trees with Tractable Combined Complexity and Efficient Updates
我们给出了一个算法来枚举树的一元二阶(MSO)查询表示的不确定树自动机的结果。在线性时间预处理(在输入树中)之后,我们可以枚举具有线性延迟的答案(在每个答案中)。我们允许在树上的更新在任何时候发生,然后我们可以在树中的对数时间之后重新开始枚举。此外,我们所有的组合复杂度在自动机中是多项式的。我们的结果遵循我们以前的基于电路的枚举算法的基础上确定性树自动机,也受到我们以前的结果的启发,在文档speries的上下文中的单词和非确定性顺序扩展变量集自动机。我们扩展这些结果,并将它们与最近的树平衡计划Niewerth,使我们的枚举结构支持更新的基础树在对数时间(叶插入,叶删除,和节点重新标记)。我们的结果意味着,对于MSO查询与自由的一阶变量,我们可以枚举的结果与线性预处理和常数延迟和更新的基础树在对数时间,这改善了几个已知的结果的话和树。从数据结构的研究下界的基础上,我们还无条件地表明,我们的算法的更新时间的双对数因子是最佳的。因此,与其他设置不同,不可能存在具有恒定更新时间的算法。
2019-08-27 cs.DB cs.DS cs.FL
A Finite Axiomatisation of Finite-State Automata Using String Diagrams
本文提出一种基于字符串图的有限状态自动机图解方法,实现了语言等价性的有限公理化,并将Kleene星号分解为更基本的代数块。
2023-02-14 cs.FL cs.LO
Run-Length Encoded Nondeterministic KMP and Suffix Automata
我们提出了一种新的位并行表示,基于行程长度编码的非确定性KMP和后缀自动机的字符串$P$至少有两个不同的符号。我们的方法针对的是小字母表上的长字符串的情况,并补充了Cantone et al.(2012)的方法,该方法对大字母表上的长字符串有效。我们的编码需要$O((σ+ m)\lceil ρ/ w\rceil)$空间,并允许一个模拟的自动机在一个字符串上的时间$O(\lceil ρ/ w\rceil)$每个过渡,其中$σ$是字母表的大小,$m$是$P$的长度,$ρ$是行程长度编码的长度$P$和$w$是机器字的大小位。输入字符串可以以未编码或游程长度编码的形式给出。
2014-12-17 cs.DS cs.FL
Twinning automata and regular expressions for string static analysis
Ca’ Foscari University of Venice(威尼斯大学);JuliaSoft S.r.l.(JuliaSoft有限公司)
本文提出基于抽象解释理论的Tarsis抽象域,通过有限状态自动机近似字符串值,利用字符串字母表提升分析精度,通过实验验证其优于现有方法。
2020-06-04 cs.FL cs.SE
A Myhill-Nerode theorem for automata with advice
带有通知的自动机是一个有限状态自动机,它可以访问一个额外的固定的无限字符串,称为通知带。我们完善的Myhill-Nerode定理来表征的语言有限字符串的自动机接受的意见。我们对树自动机做同样的建议。
2012-10-09 cs.FL cs.LO
Z3-Noodler: An Automata-based String Solver (Technical Report)
Z3-Noodler是一个基于自动机的字符串求解器,通过稳定化算法求解带正则约束的单词方程,在众多基准上超越现有求解器,并与其他求解器互补,适合作为求解器组合的候选。
2023-10-17 cs.FL cs.LO
Power of Randomization in Automata on Infinite Strings
概率Büchi自动机(PBA)是随机的,有限状态自动机,处理无限长度的输入字符串。基于为接受概率选择的阈值,可以定义不同的语言类别。在本文中,我们提出了一些结果,澄清了这种机器的力量和他们定义的语言的属性。我们关注的广泛主题如下。我们目前的结果的可判定性和精确的复杂性的空虚,普遍性和语言包容性的问题,这样的机器,从而回答中央使用这些模型在形式化验证的问题。其次,我们对PBAs识别的语言进行了拓扑刻画,证明了虽然一般的PBAs可以识别非正则语言,但在拓扑上,这些语言与ω-正则语言一样简单。最后,我们介绍了层次PBAs,这是PBAs的语法限制形式,易于处理,准确地捕捉类的ω-正则语言。
2011-09-28 cs.FL cs.LO
A String Diagrammatic Axiomatisation of Finite-State Automata
我们开发了一个完全图解的方法,有限状态自动机理论的基础上,重新解释他们通常的状态转换图形表示为二维语法的字符串图。此外,我们提供了一个等式理论,完全公理化语言等价在这个新的设置。这一理论有两个显著特点。首先,Kleene星是一个衍生概念,因为它可以分解成更原始的代数块。其次,建议的axiomatisation是有限的-结果是证明不可能获得的一维语法的正则表达式。
2020-11-04 cs.FL cs.LO math.CT
An automata-based test for bricks over string algebras
Indian Institute of Technology Kanpur(坎普尔印度理工学院)
本文提出多入口逆自动机,用于研究字符串代数中砖块与Sturmian词的关系,揭示有限/无限字符串模的砖块性质。
2026-03-19 cs.FL math.RT
Implicit automata in λ-calculi III: affine planar string-to-string functions
本文通过非交换仿射逻辑的λ-项刻画一阶字符串转换,扩展星自由语言结果,利用Krohn-Rhodes分解和双向可逆平面换能器证明双向包含,并处理范畴单位非终对象的挑战。
2024-12-07 cs.FL cs.LO
String Diagrammatic Trace Theory
本文将幺半范畴中的形式语言理论扩展至多类对称情形,通过引入对称幺半自动机统一了 Mazurkiewicz 迹语言与 Zielonka 异步自动机,并利用字符串图推导迹的串行化。
2023-06-28 cs.FL math.CT
Sampling from Stochastic Finite Automata with Applications to CTC Decoding
Google Research(谷歌研究院)
随机有限自动机自然地出现在许多语言和语音处理任务中。它们包括随机受体,代表随机字符串上的某些概率分布。我们考虑有效抽样的问题:从随机自动机和变换的概率分布中抽取随机字符串变量。我们表明,路径采样是有效的,可以是有效的,如果一个有限自动机的ε-图是非循环的。我们提供了一个算法,确保这一点,通过合并ε-周期内强连接组件。采样在字符串的非内射变换的存在下也是有效的。我们说明了这一点,在解码的上下文中的连接时间分类(CTC),预测概率产生辅助序列转化为较短的标签字符串。我们可以从转换后的标记分布中有效地采样,并将其用于两种不同的策略中,以找到最可能的CTC标记。
2019-05-21 cs.CL cs.FL cs.LG
A Büchi-Elgot-Trakhtenbrot theorem for automata with MSO graph storage
本文提出 MSO 图存储类型并证明相应的 Büchi-Elgot-Trakhtenbrot 定理,涵盖字符串与图两种情形,并证明自动存储类型及迭代下推存储类型均可 MSO 表达。
2020-08-20 cs.FL
Time complexity for deterministic string machines
The Hebrew University of Jerusalem(耶路撒冷希伯来大学)
本文通过范畴论中的字符串图形式化自动机的组合语言,研究确定性有限状态变换的运行时间与表达能力,并给出多项式时间保证的充分条件。
2026-06-24 cs.CC cs.FL math.CT
Efficient Enumeration Algorithms for Annotated Grammars
我们引入注释语法,上下文无关文法的扩展,它允许终端上的注释。我们的模型扩展了标准的概念,定期spectrum,更有表现力比提取语法最近推出的Peterfreund。我们研究了注释语法的枚举问题:固定一个语法,并给定一个字符串作为输入,枚举所有注释的字符串,形成一个词派生的语法。我们的第一个结果是一个算法,明确的注释语法,预处理输入字符串在立方时间和枚举所有的注释输出线性延迟。这改进了Peterfreund的结果,该结果需要五次时间预处理来实现该延迟界限。然后,我们研究如何减少预处理时间,同时保持相同的延迟范围,通过对语法作出额外的假设。具体来说,我们提出了一类语法,只有一个派生形状的所有输出,我们可以枚举与二次时间预处理。我们还给出了类,推广定期spectrometry的线性时间预处理足够。
2022-05-17 cs.DS cs.FL
Regular Functions, Cost Register Automata, and Generalized Min-Cost Problems
受正则语言理论在有限状态系统形式化验证中的成功应用的启发,人们重新对发展从字符串到数值的可分析函数理论产生了兴趣,该理论可以为分析有限状态系统的{ \em定量}性质提供基础。在本文中,我们提出了一个确定性的模型关联成本与字符串的参数化操作的兴趣(如添加,缩放,和$\min$),{ \em正则性}的概念,提供了一个衡量表现力的尺度,并研究决策问题和理论性质的成本函数类。我们的规则性的定义依赖于串到树转换器的理论,并允许将成本与以未来事件的规则属性为条件的事件相关联。我们的{ \em成本寄存器自动机}模型允许使用多个“只写”寄存器计算常规函数,这些寄存器的值可以使用允许的操作集进行组合。我们表明,经典的最短路径算法,以及算法设计的计算{ \em折扣成本},可以采用解决最小成本问题,在我们的模型中指定的功能更一般的类。带有$\min$和增量的成本寄存器自动机给出了一个确定性模型,它等价于{ \em加权自动机},一个被广泛研究的非确定性模型,这种连接导致了新的见解和新的开放问题。
2012-02-21 cs.FL cs.LO
Second-Order Finite Automata
传统上,有限自动机理论一直被用来作为一个框架,表示可能无限的字符串集。在这项工作中,我们介绍了二阶有限自动机的概念,一种形式主义,结合有限自动机与有序决策图,其目的是表示可能无限{ \em集}的字符串。我们的主要结果表明,二阶有限自动机可以相对于它们所代表的二阶语言被规范化。使用这个标准化的结果,我们表明,由二阶有限自动机表示的字符串集合的集合是封闭的通常的布尔运算下,如联合,交叉,差异,甚至在一个合适的概念互补。此外,交集和包含的空性是可判定的。我们提供了二阶自动机的两个算法应用。首先,我们证明了几个宽度/大小最小化问题的确定性和不确定性的ODD是可解的固定参数易处理的时间时,参数化的输入ODD的宽度。特别是,我们的研究结果意味着FPT算法相应的宽度/大小最小化问题的有序二元决策图(OBDDs)与一个固定的变量排序。以前,只有在输入OBDD的大小上花费指数时间的算法才被称为宽度最小化,即使对于恒定宽度的OBDD也是如此。第二,我们表明,对于每个$k$和$w$可以计数的不同功能的数量可计算的ODD的宽度最多$w$和长度$k$在时间$h(|Σ|,w)\cdot k^{O(1)}$,为一个合适的$h:\mathbb{N}\times \mathbb{N}\rightarrow \mathbb{N}$。这在显式枚举所有这样的函数所需的时间上呈指数级地改进,这在ODD的宽度参数$w$和长度…
2021-08-29 cs.CC cs.FL
Automata and Reduced Words in the Free Group
我们考虑了一些关于形式语言的问题,这些问题是在定义字母、单词和语言的逆时出现的。语言在自由幺半群上的约化表示是它在自由群中的唯一等价表示。我们证明了正则语言类在约简表示下是封闭的,而上下文无关语言类则不是。我们还给出了正则语言的约简表示的状态复杂度的上界,并证明了正则语言的最短可约串长度的上界和下界。最后,我们证明了正则语言中等价于词的所有词的集合可以是非正则的,并且正则语言在取约化表示的广义形式下是不封闭的.
2009-10-23 cs.FL
Implicit automata in typed $λ$-calculi II: streaming transducers vs categorical semantics
本文将正则字符串转换刻画为带加法算子的线性 λ-演算程序,通过编码无复制流式字符串转换器并利用范畴语义学建立等价关系,进而将结果推广至树结构并揭示其与线性逻辑的联系。
2021-08-25 cs.FL cs.LO
Succinct Representation for (Non)Deterministic Finite Automata
确定性有限自动机是自动机理论中最简单、最实用的计算模型之一。它们的概念扩展是非确定性有限自动机,它也有着广泛的应用。在这篇文章中,我们通过简洁的数据结构来研究这些模型,我们的最终目标是使用信息理论上的最佳比特数对这些数学对象进行编码,并有效地支持对它们的查询。为了这个目标,我们首先设计了一个简洁的数据结构,用于表示任何确定性有限自动机$\mathcal{D}$具有$n$状态的$σ$ -字母表$Σ$使用$(σ-1) n\log n + O(n \log σ)$位的空间,它可以确定,给定一个输入字符串$x$的$Σ$,$\mathcal{D}$是否接受$x$在$O(|x| \log σ)$时间,使用恒定字的工作空间。当输入的确定性有限自动机是非循环的时,我们不仅可以将上述的空间限制显著地提高到$(σ-1) (n-1)\log n+ 3n + O(\log^2 σ) + o(n)$位,而且还得到了最优的字符串接受检查的查询时间。更具体地说,使用我们的简洁表示,我们可以检查一个给定的输入字符串$x$是否可以接受的非循环确定性有限自动机使用的时间成正比的$x$的长度,因此,最佳的查询时间。我们还展示了一个简洁的数据结构,用于表示一个非确定性有限自动机$\mathcal{N}$具有$n$状态的$σ$ -字母表$Σ$使用$σn^2+n$位的空间,这样,给定一个输入字符串$x$,我们可以决定是否$\…
2019-07-22 cs.DM cs.DS 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
A New Notion of Regularity: Finite State Automata Accepting Graphs
该研究提出确定性有向无环图语言的一个更弱子类,其可对应经典确定性有限状态自动机,对并交运算封闭,可应用DFA的最小化算法,为图语言研究提供新的正则性视角。
2024-09-11 cs.DM cs.FL
Learning Deterministic Finite Automata from Confidence Oracles
本文研究从置信度预言机学习确定性有限自动机(DFA)的问题,旨在构建一个在预言机高置信度区域紧密匹配其行为的DFA表示。
2023-11-18 cs.FL cs.LG
Gödel Number based Clustering Algorithm with Decimal First Degree Cellular Automata
National Institute of Technology(印度国家理工学院)
提出一种利用哥德尔数编码和一阶十进制元胞自动机可达循环的聚类算法,并通过多项基准指标验证其优于现有方法。
2024-05-08 cs.ET cs.FL cs.LG
Large Scale Geometries of Infinite Strings
本文将几何群论引入形式语言研究无穷串的大尺度几何,通过拟等距映射分类全局模式,并探讨了与Büchi automata、可计算性及算法随机性相关的五个核心问题。
2024-06-01 cs.FL cs.LO
Model Checking Regular Language Constraints
即使是最快的SMT求解器在处理来自真实程序的正则表达式时也会遇到性能问题。由于这些性能问题通常来自问题表示(例如,非确定性有限自动机得到确定和正则表达式得到展开),我们重新审视布尔有限自动机,它允许直接和自然的表示任何正则语言的布尔组合。将IC3模型检验算法应用于布尔有限自动机,不仅可以有效地回答空性和普适性问题,而且通过扩展,可以判定多变量串成员问题的可满足性。我们证明了所产生的系统的有效性,一些流行的基准和正则表达式。
2017-08-30 cs.FL cs.LO cs.SC