Minimization of Automata
这一章关注的是最小化有限自动机的算法的设计和分析。在文本处理、图像分析、语言学计算机科学和许多其他应用的框架中，获得最小自动机是有限自动机工具的使用和实现中的一个基本问题。最小化算法主要有两类。第一种是对状态集的划分进行一系列细化，第二种是对状态进行一系列融合或合并。Hopcroft和Moore算法属于第一类，Revuz的无环自动机的线性时间最小化算法属于第二类。我们的研究之一是比较的性质摩尔和Hopcroft的算法。这在两种算法中提供了一些新的见解。正如我们将看到的，这些算法在行为和复杂性上都有很大的不同。特别是，我们表明，它是不可能的模拟计算的算法之一，由其他。我们描述了所谓的局部自动机融合的最小化算法。最小化的一个特殊情况是构造有限集合的最小自动机。我们简要考虑这种情况，并特别描述增量算法。最后，我们考虑的情况下，更新一个最小的自动机时，一个字被添加或删除的集合，它承认。
2010-12-30 cs.FL
On the Complexity of Equivalence and Minimisation for Q-weighted Automata
本文研究有理数域Q上带转移权的自动机的等价性和极小化的计算复杂性。我们使用多项式的身份测试和隔离引理，以获得复杂性的界限，集中在类NC的问题在P可解决的多对数并行时间。对于有限的Q-加权自动机，我们给出了一个随机NC过程，要么输出两个自动机是等价的，要么返回一个字，他们不同。我们还给出了一个NC程序，决定是否给定的自动机是最小的，以及随机NC程序，最小化的自动机。我们考虑具有奖励的概率自动机，类似于马尔可夫决策过程。对于这些自动机，我们考虑两个等价的概念：期望等价和分布等价。前者要求两个自动机在每个输入词上具有相同的期望奖励，而后者要求每个输入词在每个自动机中诱导相同的奖励分布。对于这两个概念，我们给出了算法来决定等价减少到等价的Q-加权自动机。最后，我们证明了Q-加权下推自动机的等价问题是对数空间等价于多项式恒等式检验问题。
2013-03-01 cs.FL
Minimization of semilinear automata
我们研究有限的确定性自动机集与非齐次原子：整数与继任者。由于在这一背景下有无数的确定性有限自动机，我们将注意力集中在具有半线性转移函数的自动机上。主要结果是半线性自动机的一个极小化过程。证明是微妙的，是指存在的Presburger算术与整除谓词的可判定性。有趣的是，最小化不是通过标准的分区细化过程，我们证明了这个过程不一定终止半线性自动机。
2012-10-17 cs.FL cs.LO
Optimal Spectral-Norm Approximate Minimization of Weighted Finite Automata
我们解决近似最小化问题的加权有限自动机（WFAs）的权重在$\mathbb{R}$，在一个字母表：计算最好的近似的一个WFA给定的状态数的限制。这项工作是基于Adamyan-Arov-Krein近似理论，一个显着的收集结果的近似汉克尔算子。除了其内在的数学相关性，该理论已被证明是非常有效的模型简化。我们适应这些结果的框架加权自动机在一个字母表。我们提供了理论上的保证和边界的质量近似的频谱和$\ell^2$规范。我们开发了一个算法，根据汉克尔算子的性质，返回的谱范数的最佳逼近。
2021-05-17 cs.FL
Revisiting the Equivalence Problem for Finite Multitape Automata
确定性多带自动机（或转换器）的判定等价性是一个长期存在的开放问题，直到Harju和Karhumäki在20世纪90年代初解决。他们的可判定性证明产生了一个co_NP上界，但显然对问题的复杂性知之甚少。在本文中，我们给出了另一种证明的可判定性，它遵循的基本策略的Harju和Karhumaki，但取代他们使用群论的结果矩阵代数。从我们的证明，我们得到一个简单的随机算法，决定语言等价的确定性多带自动机，更一般地说，多重性等价的非确定性多带自动机。该算法只涉及矩阵求幂，并在多项式时间内运行每个固定数量的磁带。如果两个输入自动机是不等价的，那么算法输出一个它们不同的词。
2013-05-02 cs.FL
Reducing Transducer Equivalence to Register Automata Problems Solved by "Hilbert Method"
在过去的几十年中，代数的经典结果，包括希尔伯特的基本定理，在形式语言中有各种应用，包括Escherichfeucht猜想的证明，HDT0L序列等价的可判定性，以及函数树到串转换器的等价问题的可判定性。在本文中，我们研究了上述代数方法的范围，特别是适用于寄存器自动机的等价问题。我们提供了两个结果，一个阳性，一个阴性。结果表明，无序森林上的MSO变换是等价的。否定的结果来自于尝试将该方法扩展到确定宏树换能器的等效性。我们减少了宏树换能器等价的等价问题，一类寄存器自动机自然相关的我们的方法。然后，我们证明后一个问题是不可判定的。
2019-01-04 cs.FL
Equivalence Testing of Weighted Automata over Partially Commutative Monoids
我们研究\emph{multiplicity equivalence}测试自动机部分交换幺半群（PC幺半群），并在特殊情况下，利用结构的基础非交换图的幺半群显示有效的算法。具体地说，如果pc幺半群的非对易图的团覆盖数（覆盖该图的最小团数）为常数，我们得到了一个确定性的拟多项式时间算法。作为结果，我们还得到了$k$ -带自动机多重数等价性检验和确定性$k$-带自动机对常数$k$的等价性检验的第一个确定性拟多项式时间算法.在此之前，Worrell [ICALP 2013]给出了上述问题的随机多项式时间算法。我们还考虑了pc幺半群的非交换图的覆盖组成的最多$k$集团和星形图的任何常数$k$。我们得到了这类幺半群上自动机多重等价性检验的随机多项式时间算法。
2020-05-31 cs.FL
On the Complexity of the Equivalence Problem for Probabilistic Automata
检验两个概率自动机的等价性已被证明是有效地建立概率系统的各种行为和匿名性的关键问题。在最近的实验中，基于多项式同一性测试的随机等价性测试优于确定性算法。在本文中，我们表明，多项式身份测试产生有效的算法，各种概括的等价问题。首先，我们提供了一个随机NC程序，也输出一个反例跟踪的情况下，不等价。其次，我们将展示如何检查等价性两个概率自动机（累积）奖励。我们的算法运行在确定性的多项式时间，如果奖励计数器的数量是固定的。最后，我们证明了概率可见下推自动机的等价问题是对数空间等价的算术电路同一性测试问题，这是决定由算术电路表示的多项式是否为同零。
2012-01-06 cs.FL
Nondeterministic automata: equivalence, bisimulations, and uniform relations
在本文中，我们研究了对等的不确定自动机配对的概念，互模拟与最近推出的概念的一致关系。在这种共生关系中，统一关系作为等价关系，将两个可能不同的非确定性自动机的状态联系起来，互模拟确保了这些自动机的过渡，初始和最终状态的兼容性。我们定义了六种类型的互模拟，但由于对偶性，我们讨论其中三种：向前，向后向前和弱向前互模拟。对于这三种类型的互模拟，我们提供了一个程序，决定是否有这种类型的互模拟之间的两个自动机，当它存在时，相同的程序计算最大的。我们还证明了两个自动机之间存在一致的前向互模拟当且仅当这些自动机上的最大前向互模拟等价的因子自动机是同构的。我们证明了一个类似的弱向前互模拟定理，使用的概念，而不是同构的弱向前同构。我们还给出了解释所考虑的互模拟类型之间的关系的例子。
2011-02-26 cs.FL
A Canonical Form for Weighted Automata and Applications to Approximate Minimization
我们研究的问题，构造近似的加权自动机。加权有限自动机与有理级数理论有着密切的联系。有理级数是从字符串到实数的函数，可以通过有限WFA计算。其中，这包括由隐马尔可夫模型和概率自动机生成的概率分布。有理级数和WFA之间的关系类似于正则语言和普通自动机之间的关系。与这种有理级数相关联的是称为汉克尔矩阵的无限矩阵，它在极小WFA理论中起着重要作用。我们的贡献是：（1）基于有限WFA的表示，计算这种无限Hankel矩阵的奇异值分解（SVD）的有效过程;（2）基于这种SVD分解的有限WFA的新标准形;（3）构造给定WFA的近似最小化的算法。我们的近似最小化算法的目标是从一个最小的WFA开始，并产生一个较小的WFA，在一定意义上接近给定的。近似自动机的期望大小作为输入给出。我们给出的界限描述如何以及近似模拟的行为，原来的WFA。
2015-04-24 cs.FL
Syntactic Minimization of Nondeterministic Finite Automata
非确定性自动机可以被看作是实现确定性自动机的简洁程序，即完整的规范。将一个给定的确定性自动机转换成一个小的非确定性自动机在计算上是非常困难的;事实上，随之而来的决策问题是PSPACE完全的。这份文件与现状形成鲜明对比。我们限制注意亚原子的非确定性自动机，其个别国家接受工会的语法同余类。他们是一般足以涵盖几乎所有的结构性结果有关的非确定性状态极小。我们证明了将识别正则语言的么半群转换为小的亚原子受体对应于NP完全问题。NP证书是涉及句法幺半群上的关系的简单方程的解。我们还考虑了原子不确定自动机的子类介绍Brzozowski和Tamm。给定一个确定性自动机和另一个反向语言，计算小原子受体被证明是NP-完全的类似证书。我们的复杂性结果出现从代数表征（亚）原子受体的确定性自动机与半格结构，结合等价的类别，导致简洁的表示。
2021-07-09 cs.FL
On the Power of Automata Minimization in Reactive Synthesis
在人工智能应用中，时态逻辑经常被用来描述时态属性。最流行的语言是线性时态逻辑（Linear Temporal Logic，LTL）。最近，有限迹上的LTL，LTLf，已经在几种情况下进行了研究。为了对LTLf进行推理，通常将公式编译成确定性有限自动机（DFA），作为中间语义表示。此外，由于DFA具有规范表示的事实，可以应用有效的最小化算法来最大限度地减少DFA大小，从而有助于加速后续计算。在这里，我们提出了一个深入的调查两个经典的最小化算法，即Hopcroft和Brzozowski算法。更具体地说，我们展示了如何将这些算法应用于半符号（显式状态，符号转换函数）自动机表示。然后，我们比较这两种算法的上下文中的LTLf合成框架，从LTLf公式。虽然早期的研究比较两种算法从随机生成的自动机的结论是，没有算法占主导地位，我们的研究结果表明，从LTLf公式，Hopcroft的算法是最好的选择，在反应合成的背景下。更深入的分析解释了为什么Brzozowski算法的假定优势在实践中没有实现。
2021-09-17 cs.FL
Minimization of Visibly Pushdown Automata Using Partial Max-SAT
研究了不确定弱层次可视下推自动机的状态空间约简问题。VPA识别上下文无关语言的一个健壮且算法上易于处理的片段，这对于建模程序是自然的。我们定义了一个等价关系，这是足够的语言保持的VPA的解释。我们的定义允许合并具有不同行为的状态，只要它们对可达的等价堆栈显示相同的行为。我们编码存在这样的关系作为一个布尔部分最大可满足性（PMax-SAT）问题，并提出了一个算法，快速找到满意的分配。这些分配是PMax-SAT问题的次优解决方案，但仍然可以导致状态的显着减少。我们将我们的方法集成在基于自动机的软件验证器Ultimate Automizer中，并在软件验证竞赛SV-COMP的基准测试中显示性能改进。
2017-04-18 cs.FL
On Minimization and Learning of Deterministic $ω$-Automata in the Presence of Don't Care Words
RWTH Aachen University（亚琛工业大学）
研究在存在不要关心词情况下确定性ω-自动机的最小化问题，证明了在任意不要关心词集合下确定性奇偶自动机优先级可高效最小化，并指出对于具有信息性右同余的确定性奇偶自动机，最小化问题为NP难。
2023-07-10 cs.FL
Optimal Approximate Minimization of One-Letter Weighted Finite Automata
针对单字母实权重无冗余加权有限自动机（WFAs）的近似最小化问题，本文基于汉克尔矩阵重述问题并利用AAK理论，提出谱范数下的最优解及多项式时间算法，给出谱范数和ℓ²范数的近似质量界。
2023-05-31 cs.FL
Distribution-based Bisimulation and Bisimulation Metric in Probabilistic Automata
概率自动机是拉宾在1963年作为语言接受者引入的。两个自动机是等价的，当且仅当它们以相同的概率接受每个单词。另一方面，在过程代数领域，Segala于1995年重新提出了概率自动机，它比Rabin的自动机更具有一般性。互模拟已经提出了Segala的自动机来表征它们之间的等价性。到目前为止，这两个概念的等价性和他们的特点，主要是独立的研究。在本文中，我们考虑Segala的自动机，并提出了一个新的概念，基于分布的互模拟加入现有的等价性和双相似性。我们通过研究基于分布的互模拟度量证明了我们的定义的实用性，这产生了一个强大的概念，相当于拉宾的自动机。我们比较我们的互模拟的概念，一些现有的基于分布的互模拟，并讨论其组合性和关系，跟踪等价。最后，我们展示了所有关系的可判定性和复杂性。
2015-12-16 cs.FL
Minimization of Büchi Automata using Fair Simulation
我们提出了一个算法，它减少了规模的Büchi自动机使用公平模拟。其时间复杂度为$\mathcal{O}(|Q|^4 \cdot |Δ|^2)$，空间复杂度为$\mathcal{O}(|Q| \cdot |Δ|)$。模拟是最小化$ω$ -自动机如Büchi自动机的常用方法。直接模拟、延迟模拟和公平模拟是不同类型的模拟。正如我们将展示的，基于直接或延迟模拟的最小化在概念上是简单的。而基于公平模拟的算法则比较复杂。然而，公平模拟允许自动机的更强的最小化。此外，我们说明了算法背后的理论，涵盖在实践中有用的优化，给出实验结果，并比较我们的技术与其他最小化策略。
2016-03-03 cs.DS cs.FL
Late Weak Bisimulation for Markov Automata
弱双相似性是马尔可夫自动机的一个基于分布的等价概念。它作为马尔可夫自动机上的粗略合理的行为等价已经得到了一些普及。本文研究了一个严格粗糙的概念：晚弱双相似性享有有价值的属性，如果限制到重要的子类的标记：迹分布等价隐含的部分信息标记，和组合性保持分布式标记。因此，两个调度程序类的交集跨越了马尔可夫自动机的一个更粗糙但仍然合理的组合理论。
2014-01-14 cs.FL
Equivalence of Deterministic Weighted Real-time One-Counter Automata
本文引入了确定性加权实时单计数器自动机（DWROCA），并为其等价性问题提供了更简证明与更优多项式时间算法。
2024-11-17 cs.FL
Systems of Graph Formulas and their Equivalence to Alternating Graph Automata
Umeå universitet（于默奥大学）；Universität Bremen（不来梅大学）；Universität der Bundeswehr München（慕尼黑联邦国防军大学）
本文提出图公式系统，证明其与交替图自动机在图语言规范上的等价性，从而建立了自动机理论与逻辑方法之间的桥梁。
2026-01-22 cs.FL
Automata Minimization: a Functorial Approach
本文提出函子框架统一自动机最小化，给出输出范畴充分条件保证最小化，提升伴随关系，并解释Choffrut与Brzozowski算法。
2020-03-20 cs.FL cs.LO
Minimization and Canonization of GFG Transition-Based Automata
本文提出一种针对转移型GFG co-Büchi词自动机的多项式时间最小化算法，并证明其最小自动机具有规范性，即安全组件同构且经α-转移饱和后完全同构。
2022-08-01 cs.FL cs.LO
Minimal Nondeterministic Finite Automata and Atoms of Regular Languages
我们研究的NFA最小化问题的原子NFA的，也就是说，NFA的每个状态的正确的语言是一个原子的工会，其中的原子的正则语言的非空的交叉的补充和非补充的语言的左分支。我们的特点是所有减少原子NFA的一个给定的语言，也就是说，那些NFA的，没有等价的状态。使用原子NFA的，我们正式Sengoku的方法NFA最小化，并证明他的方法无法找到所有最小的NFA的。我们还制定Kameda-Weiner NFA最小化方面的杂质和原子。
2013-01-23 cs.FL
Hyper-Minimization for Deterministic Weighted Tree Automata
超最小化是一种允许语义有限变化的状态约简技术。给出了确定性加权树自动机的超极小化理论。与未加权的情况相比，加权的存在使情况稍微复杂化。此外，第一超最小化算法的确定性加权树自动机，加权交换半域，提供了一些实施意见，使一个有效的实施。实际上，得到了与未加权情况相同的运行时O（mlog n），其中m是确定性加权树自动机的大小，n是其状态数。
2014-05-22 cs.CC cs.DS cs.FL
A Congruence-Based Perspective on Finite Tree Automata
本文利用树上的同余关系，研究树自动机的确定化与最小化，证明了一种Brzozowski风格的最小化算法，并扩展至词自动机情形。
2021-12-21 cs.FL
Automata in the Category of Glued Vector Spaces
在本文中，我们采用了范畴理论的方法享受最小化设计的自动机类的概念。我们构造的主要实例是一类新的自动机，它们是确定性自动机和域上加权自动机之间的混合。
2017-11-16 cs.FL
When Equivalence and Bisimulation Join Forces in Probabilistic Automata
概率自动机是拉宾在1963年作为语言接受者引入的。两个自动机是等价的，当且仅当它们以相同的概率接受每个单词。另一方面，在过程代数领域，Segala于1995年重新提出了概率自动机，它比Rabin的自动机更具有一般性。互模拟已经提出了Segala的自动机来表征它们之间的等价性。到目前为止，等价的两个概念及其特征是最独立的研究。在本文中，我们考虑Segala的自动机，并提出了一个新的概念，基于分布的互模拟加入现有的等价和双相似。我们的互模拟桥梁社区中的两个密切相关的概念，并提供了一个统一的方式来研究他们的特点。我们通过研究基于分布的互模拟度量证明了我们的定义的实用性，这产生了拉宾自动机的等价性的强大概念。
2014-03-08 cs.FL cs.LO
Advanced Automata Minimization
我们提出了一个有效的算法，以减少不确定的Buchi字自动机的大小，同时保留他们的语言。此外，我们还描述了解决PSPACE完全自动机问题的方法，如普适性，等价性和包含性，适用于比以前大得多的实例（1-3个数量级）。这可以用于自动机在逻辑理论的形式化验证工具和决策过程中的应用。该算法是基于新的过渡修剪技术。这些使用基于向后和向前跟踪包含的组合的标准。由于这些关系本身是PSPACE-完全的，我们描述的方法来计算良好的近似它们在多项式时间。大量的实验表明，我们的算法的平均情况下的复杂度的规模平方。自动机的大小减少非常依赖于类的实例，但我们的算法始终优于所有以前的技术，由一个很大的保证金。我们测试了我们的算法上的Buchi自动机来自LTL公式，许多类的随机自动机和自动机来自互斥协议，并比较其性能的著名的自动机工具GOAL。
2012-10-24 cs.DS cs.FL
A Myhill-Nerode style Characterization for Timed Automata With Integer Resets
本文为带整数重置的定时自动机提出依赖常数K的Nerode风格等价，建立Myhill-Nerode定理与规范自动机，并据此设计查询复杂度为多项式的Angluin风格主动学习算法。
2024-10-03 cs.FL
Learning Realtime One-Counter Automata
本研究提出一种融合成员、等价、计数器值及部分等价查询的实时单计数器自动机学习算法，并在随机基准与JSON流验证场景中完成了效果评估。
2024-09-13 cs.FL
Testing the Equivalence of Regular Languages
最小确定性有限自动机通常用于判定正则语言的相等性。Antimirov和Mosses提出了一个重写系统来决定正则表达式的等价性，Almeida等人提出了一个改进的变体。Hopcroft和Karp提出了一个几乎线性的算法来测试两个确定性有限自动机的等价性，避免了最小化。在本文中，我们改进了最佳情况下的运行时间，提出了一个扩展的非确定性有限自动机的算法，并建立了该算法之间的关系，提出了在Almeida等人，我们还提出了一些实验比较结果。这些算法都与Rutten提出的自动机的共代数方法密切相关。
2009-07-29 cs.FL
On Shuffling and Splitting Automata
本文研究建模单词混洗与拆分的三带有限状态转换器，将其定义为 Shuffling Monoid 上的自动机，并证明拆分器的功能性及功能等价性可判定，确定性情形下等价算法关于状态数为多项式复杂度。
2024-07-02 cs.FL
Optimal Hyper-Minimization
最小确定性有限自动机（DFA）可以进一步减少在有限数量的错误为代价。最近，这样的最小化算法已经被改进为在时间O（n log n）中运行，其中n是输入DFA的状态数，由[Gawrychowski和Jewish：Hyper-minimisation made efficient. Proc. MFCS，LNCS 5734，2009]和[Holzer和Maletti：An n log n algorithm for hyper-minimizing a（minimized）deterministic automaton. Theor. Comput. Sci. 411，2010]。这两种算法都返回尽可能小的DFA，同时只提交有限数量的错误。这些算法被进一步改进以返回以增加的（二次）运行时间为代价的提交最少数量的错误的DFA。这解决了[Badr，Geffert，and Shipman：Hyper-minimizing minimized deterministic finite state automata]的一个公开问题。拉伊罗·泰奥。Inf·Appl·43，2009]。此外，对随机自动机进行了实验研究，并报告了现有算法和新算法的效果。
2011-04-15 cs.FL
Equivalence of pushdown automata via first-order grammars
给出了一阶文法互模拟等价的可判定性证明。它是Sénizergues（1998，2005）的一个结果的另一种证明，该结果包含了他对确定性下推自动机的著名可判定性问题的肯定解。所提出的证明是概念上更简单，一个特别的新颖性是，它不是作为两个半决策程序，但它提供了一个明确的算法，可能是服从复杂性分析。
2020-08-17 cs.FL cs.LO
Weighted finite automata with output
在本文中，我们证明了等价的顺序，Mealy-type和Moore-type加权有限自动机的输出，相对于各种语义，这里定义的。
2014-10-09 cs.FL
A Symbolic Decision Procedure for Symbolic Alternating Finite Automata
我们引入符号交替有限自动机（S-AFA）作为一个表达，简洁，可判定的模型，用于描述任意字母表上的有限序列集。s-AFA上的布尔运算具有线性复杂度，这与非交替符号自动机的交和并的二次成本形成鲜明对比。由于这种简洁性，空性和等价性检查是PSpace困难的。我们介绍了一种算法，用于检查两个s-AFA的等价性的基础上互模拟同余。该算法允许我们利用SAT和SMT求解器的能力来有效地搜索s-AFA的状态空间。我们评估我们的决策过程中的两个验证和安全应用：1）检查可满足性的线性时序逻辑公式在有限的痕迹，2）检查等价的布尔组合的正则表达式。我们的实验表明，我们的技术往往优于现有的技术，它可以在这两个应用程序中是有益的。
2016-10-06 cs.FL
Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata
本文提出轨道有限集张成的向量空间理论，并据此给出加权寄存器自动机等价性的指数时间判定算法，固定寄存器数时降为多项式时间，同时以相同复杂度改进无歧义寄存器自动机的语言等价性判定。
2024-05-03 cs.FL
Equivalence Checking and Intersection of Deterministic Timed Finite State Machines
人们对定义具有丰富时间的自动机模型越来越感兴趣，例如用时钟扩展的有限自动机（时间自动机）。在本文中，我们研究确定性时间有限状态机（TFSM），即，有限状态机具有单个时钟、定时保护和超时，其将定时输入字转换为定时输出字。我们解决了等价性检查的问题，通过定义一个互模拟定时FSM的untimed的，反之亦然。此外，我们应用这些互模拟关系来建立两个定时有限状态机的交集，通过对它们进行反定时，相交并转换回定时交集。
2021-03-08 cs.FL
Learn with SAT to Minimize Büchi Automata
我们描述了一个不确定的Büchi自动机（NBA）的最小化过程。对于一个自动机A，另一个具有最小状态数的自动机A_min在SAT求解器的帮助下学习。这是通过连续计算自动机A'来完成的，自动机A'在某种意义上近似A，它们接受给定的有限的正例集，拒绝给定的有限的负例集。在程序的过程中，这些示例集被连续地增加。因此，我们的方法可以被看作是一个通用的学习算法的基础上的“最低限度的适当的老师”的意义上的盎格鲁。我们使用SAT求解器为给定的正面和负面示例集找到NBA。我们通过构造确定性奇偶自动机来使用互补来检查以这种方式计算的候选者与A的等价性。不对等会产生新的正面或负面例子。我们的方法被证明是成功的完全采样的小自动机和相当多的例子较大的自动机。我们成功地运行了超过一万个自动机的最小化，其中大多数最多有十个状态，包括所有可能的自动机的补充与两个状态和字母表大小3，并讨论结果和运行时;单个例子有超过100个状态。
2012-10-09 cs.FL
Deterministic Timed Finite State Machines: Equivalence Checking and Expressive Power
人们对定义随时间而丰富的自动机模型越来越感兴趣。例如，时间自动机被引入作为用时钟扩展的自动机。在本文中，我们研究了时间有限状态机（TFSMs）的模型，即，用时间丰富的FSM，它接受定时输入单词并生成定时输出单词。在这里，我们讨论了具有单个时钟的TFSM的一些模型：具有定时保护的TFSM、具有超时的TFSM以及具有定时保护和超时的TFSM。我们解决了所有三个模型的等价性检查的问题，我们比较他们的表达能力，特征的TFSM的子类定时警卫和TFSM的超时是等价的。
2014-08-26 cs.FL
Weak equivalence of higher-dimensional automata
本文提出高维自动机的弱等价概念，结合迹语言与同调语言刻画独立结构，并证明其与张量积、余积兼容，支持通过立方体合并与折叠实现化简。
2021-05-16 cs.FL cs.LO math.AT
Parikh Image of Pushdown Automata
我们比较下推自动机（PDA的短）对其他表示。首先，我们表明，有一个家庭的PDA在一元字母表的$n$状态和$p \geq 2n + 4$堆栈符号，接受一个单一的长字，每一个等价的上下文无关文法需要$Ω(n^2(p-2n-4))$变量。这个家庭表明，经典的算法转换PDA到一个等效的上下文无关文法是最佳的，即使当字母表是一元。此外，我们观察到，语言等价和Parikh等价，它忽略了符号之间的顺序，这个家庭相吻合。我们的结论是，当假设这种较弱的等价性，转换算法也是最佳的。其次，Parikh定理激发了PDA与有限状态自动机的比较。特别是，同一个家庭的一元PDA给出了一个下界的状态数的每一个帕里克等价的有限状态自动机。最后，我们研究的情况下，一元确定性PDA。我们展示了一个新的建设转换成一个等价的上下文无关文法，达到最佳已知的界限一元确定性PDA。
2017-06-26 cs.FL
On the Equivalence Checking Problem for Deterministic Top-Down Tree Automata
针对自顶向下确定性有限树自动机（DFTAs）的状态语言等价判定问题，提出将其转化为语言理论方程系统可解性检查的高效算法，通过代入与冲突检测开发判定程序，并证明其正确性、终止性及$O(n^2)$最坏时间复杂度。
2025-04-05 cs.FL math.LO
A Characterization of Totally Compatible Automata
有限集合上的每个函数都定义了一个等价关系，因此，一个划分被称为函数的核。使得每个可能的划分都是一个词的核的自动机被称为完全相容的。这样的自动机的一个特征，连同一个算法来识别它们在多项式运行时间的状态数。
2021-10-11 cs.FL
Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests
我们首先提出了一个大字母表上的有限自动机的语言等价性检查算法。我们使用符号自动机，其中的过渡函数是competently表示使用（多端）二进制决策图（BDD）。其关键思想在于通过符号化地探索可达对来计算互模拟，从而避免冗余。这个想法可以结合现有的优化，我们特别显示了一个很好的集成与不相交集森林数据结构从Hopcroft和卡普的标准算法。然后，我们考虑Kleene代数与测试（KAT），代数理论，可用于验证从编译器优化到网络编程分析的各个领域。这个理论是可判定的减少到语言等价的自动机上的保护字符串，一种特殊的自动机，有指数大的字母。我们提出了几种方法，允许构造符号自动机的KAT表达式，根据Brzozowski的衍生物或标准的自动机结构。总而言之，这导致了用于确定KAT表达式的等价性的有效算法。
2014-07-09 cs.FL cs.LO
Active Automata Learning with Advice
本文提出一种结合主动自动机学习与演绎推理的扩展框架，通过字符串重写系统提供建议以推断查询答案，从而减轻教师负担并显著降低查询复杂度。
2025-08-14 cs.FL
Complexity of Equivalence and Learning for Multiplicity Tree Automata
University of Oxford（牛津大学）
我们考虑多重树自动机的等价和学习的复杂性，即，加权树自动机我们首先表明，等价问题是对数空间等价的多项式身份测试，其复杂性是一个长期的开放问题。其次，我们推导出的查询数量的下界需要学习多重树自动机在Angluin的精确学习模型，在任意和固定的字段。Habrard和Oncina（2006）给出了多重树自动机的精确学习算法，其中查询的数量与目标自动机的大小和由教师返回的最大反例（表示为树）的大小成比例。然而，最小的树反例可以是目标自动机的指数大小。因此，上述算法在目标自动机的大小上不以时间多项式运行，并且在下界内具有指数的查询复杂度。假设一个教师返回最小DAG表示的反例，我们给出了一个新的精确学习算法的查询复杂度是二次的目标自动机的大小，几乎匹配的下限，并提高了最好的以前已知的算法的指数因子。
2014-11-27 cs.FL cs.LG
Algorithms and fine-grained complexity for nondeterministic and symmetric difference automata
University of Warwick（华威大学）；Stellenbosch University（斯坦伦布什大学）
研究对称差自动机（XNFA）的接受、空性和等价问题的细粒度复杂性，通过随机化归约和多项式模糊度假设，给出比一般情况更快的算法。
2026-07-02 cs.FL
Fast Coalgebraic Bisimilarity Minimization
共代数双相似性最小化推广经典自动机最小化的一大类自动机，其过渡结构指定的函子，包括强，加权，概率双相似性。这提供了将双相似性最小化转化为现成技术的诱人可能性，而不必为每种新类型的自动机开发新算法。不幸的是，目前还没有一个完全通用的、高效的、能够处理大型系统的算法。我们提出了一个通用的算法，最小化余代数在任意函子的范畴内的集合，只要行动上的态射是充分可计算的。函子最多对特定于函子的操作进行$\mathcal{O}(m \log n)$调用，其中$n$是状态数，$m$是余代数中的转换数。虽然更专业的算法可以比我们的算法快（通常是$\mathcal{O}(\frac{m}{n})$的一个因素），我们的算法特别适合于有效的实现，我们的工具Boa通常使用更少的时间和内存在现有的基准测试，可以处理更大的自动机，尽管更通用。
2022-11-17 cs.FL
Bisimulations for fuzzy automata
University of Ni s, Faculty of Sciences；University of Kragujevac, Technical faculty in Ca cak, Svetog Save 65, P. O. Box 131, 32000 Ca cak, Serbia
互模拟已被广泛应用于计算机科学的许多领域，以模拟各种系统之间的等价性，并减少这些系统的状态数，而统一的模糊关系最近被引入作为一种手段来模拟两个可能的不同集合的元素之间的模糊等价性。在这里，我们使用这两个概念的连接作为一个强有力的工具，在模糊自动机之间的等价性的研究。证明了模糊自动机$\cal A$和$\cal B$之间的一致模糊关系是前向互模拟的当且仅当其核和上核是$\cal A$和$\cal B$上的前向互模拟模糊等价，并且因子模糊自动机之间关于这些模糊等价存在一种特殊的同构.因此，我们得到模糊自动机$\cal A$和$\cal B$是UFB等价的，即，它们之间存在一致的前向互模拟，当且仅当$\cal A$和$\cal B$的因子模糊自动机之间关于它们的最大前向互模拟模糊等价存在特殊的同构。这一结果将UFB-等价性的检验问题归结为模糊自动机同构性的检验问题，而模糊自动机同构性的检验问题又与图同构问题密切相关。我们证明了一些类似的结果向后向前互模拟，我们指出根本的差异。由于所研究的概念的对偶性，向后和向前向后互模拟不被单独考虑。最后，我们给出了一个全面的概述确定性，非确定性，模糊和加权自动机，这是相关的互模拟的各种概念。
2011-05-05 cs.AI cs.FL
Extracting Weighted Automata for Approximate Minimization in Language Modelling
McGill University（麦吉尔大学）；Mila（米拉研究所）；Université de Montréal（蒙特利尔大学）
本文研究了语言模型的近似极小化问题。我们假设我们被赋予某种语言模型作为黑盒。我们的目标是获得一个加权的有限自动机（WFA），适合在一个给定的大小约束，并模仿原始模型的行为，同时尽量减少一些概念之间的距离黑盒子和提取的WFA。我们提供了一个算法的近似最小化的黑盒子训练的语言建模的顺序数据在一个字母表。通过将问题重新表述为Hankel矩阵，我们利用了Hankel算子近似的经典结果，即著名的Adamyan-Arov-Krein（AAK）理论。这允许我们使用谱范数来测量黑盒和WFA之间的距离。我们提供了理论上的保证，研究潜在的无限秩汉克尔矩阵的黑盒子，而不访问的训练数据，我们证明，我们的方法返回一个渐近最佳近似。
2021-07-23 cs.FL cs.LG
Note on the Infiniteness and Equivalence Problems for Word-MIX Languages
在本文中，我们提供了一个（可判定的）图形结构的表征的无限的$L(w_1, ..., w_k)$，其中$L(w_1, ..., w_k) = \{w \in A^* | |w|_{w_1} = \cdots = |w|_{w_k}\}$是一组的所有字，包含相同数量的子字出现的参数字$w_1, ..., w_k$。我们还提供了这些语言的等价性的可判定的表征。虽然这两个可判定性结果也是从更一般的已知的无模糊约束自动机的可判定性结果中得到的，但本文试图给出可判定性的一个自包含的（不需要关于约束自动机的知识）证明。
2019-10-27 cs.FL
An introduction to finite automata and their connection to logic
这是一个关于有限自动机的教程。我们提出的标准材料的确定性和最小化，以及一个帐户的等价性有限自动机和一元二阶逻辑。最后，我们介绍了句法幺半群，并作为应用给出了一阶可定义性和非周期性的等价性证明。
2011-09-21 cs.FL cs.LO
Equivalence checking for weak bi-Kleene algebra
本文刻画了允许语言等价性判定的Pomset自动机片段，证明其与序列有理表达式对应，从而给出序列有理表达式等价性可判定的新证明。
2021-08-11 cs.FL
