When Equivalence and Bisimulation Join Forces in Probabilistic Automata
概率自动机是拉宾在1963年作为语言接受者引入的。两个自动机是等价的，当且仅当它们以相同的概率接受每个单词。另一方面，在过程代数领域，Segala于1995年重新提出了概率自动机，它比Rabin的自动机更具有一般性。互模拟已经提出了Segala的自动机来表征它们之间的等价性。到目前为止，等价的两个概念及其特征是最独立的研究。在本文中，我们考虑Segala的自动机，并提出了一个新的概念，基于分布的互模拟加入现有的等价和双相似。我们的互模拟桥梁社区中的两个密切相关的概念，并提供了一个统一的方式来研究他们的特点。我们通过研究基于分布的互模拟度量证明了我们的定义的实用性，这产生了拉宾自动机的等价性的强大概念。
2014-03-08 cs.FL cs.LO
Markov Automata: Deciding Weak Bisimulation by means of non-naively Vanishing States
提出了一种基于马尔可夫自动机的弱互模拟判定算法。为此，定义了消失状态的不同概念（从广义随机Petri网领域已知的概念）。消失状态是必不可少的相关概念（基于状态）天真的弱互模拟和（基于分布）弱互模拟。本文提出的互模拟算法遵循划分-细化方案，具有指数时间复杂度。
2014-04-30 cs.FL cs.LO
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
Algorithms for computing the greatest simulations and bisimulations between fuzzy automata
University of Niš（尼什大学）；University of Kragujevac（克拉古耶瓦茨大学）
最近，两种类型的模拟（向前和向后模拟）和四种类型的互模拟（向前，向后，向前-向后，向后-向前互模拟）之间的模糊自动机已被引入。如果在给定的模糊自动机之间至少有一个这些类型的模拟/互模拟，则已经证明存在这种类型的最大模拟/互模拟。在本文中，对于任何上述类型的模拟/互模拟，我们提供了一个有效的算法，用于决定是否有一个模拟/互模拟这种类型之间的给定的模糊自动机，并计算最大的，每当它存在。该算法是基于在[J. J. J. Jatović，M. S. Bogdanović，On the greatest solutions to certain systems of fuzzy relation inequalities and equations，Fuzzy Sets and Systems 161（2010）3081-3113]，其归结为计算模糊关系格上的保序函数的包含在给定模糊关系中的最大后不动点。
2011-03-25 cs.AI cs.FL
Cost Preserving Bisimulations for Probabilistic Automata
概率自动机构成了并发概率系统的通用和优雅的模型。他们配备了一个组合理论支持抽象，使弱概率互模拟作为参考概念，总结抽象的效果。本文考虑了增加成本的概率自动机。它扩展了概率自动机中弱转换的概念，使得沿着弱转换产生的成本被捕获。这就产生了成本保持和成本约束的变化弱概率双相似性，我们建立组合属性相对于并行组合。此外，多项式时间的决策算法，提出了，可以有效地用于计算马尔可夫决策过程中的组合方式的回报约束抽象。
2015-02-16 cs.FL cs.LO
Bisimulations and Logics for Higher-Dimensional Automata
Norwegian University of Science and Technology（挪威科技大学）；University of Warsaw（华沙大学）；EPITA Research Lab（EPITA研究实验室）
本文提出Ipomset模态逻辑，用于刻画HDAs中的路径双向模拟，并定义单元双向模拟及其与标准双向模拟的关系。
2024-11-11 cs.FL cs.LO
Wheeler Bisimulations
University of Helsinki（赫尔辛基大学）
本文研究了双射与数据压缩的关系，提出Wheeler双射概念，展示如何通过线性时间构建最小Wheeler NFA，改进了传统双射方法。
2026-06-29 cs.DS cs.FL
Reducing Clocks in Timed Automata while Preserving Bisimulation
随着时钟数目的增加，模型检验时间自动机变得越来越复杂。因此，人们希望用尽可能少的时钟来构造一个自动机。检查是否存在一个具有较少时钟的时间自动机，使得原始自动机接受的时间语言被保留的问题是不可判定的。在本文中，我们给出了一个结构，它对任何给定的时间自动机产生一个时间双相似自动机与最少数量的时钟。此外，我们表明，这样一个自动机的最小可能数量的时钟可以构建的时间是双指数的原始自动机的时钟的数量。
2015-05-20 cs.FL cs.LO
Coalgebras for Bisimulation of Weighted Automata over Semirings
本文在半模和集合范畴的余代数框架下研究加权自动机，证明最终余代数分别刻画加权语言等价与加权互模拟，并推广了线性关系概念，提出前向划分细化算法及终止条件。
2023-01-13 cs.FL cs.LO
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
Bisimulation Equivalence of First-Order Grammars is ACKERMANN-Complete
Sénizergues（1998，2005）证明了两个具有限制静默动作的下推自动机是否弱双相似。我们提供了第一个已知的复杂性上界这个著名的问题，在等效设置的一阶文法。这ACKERMANN上限是最佳的，我们还表明，强双相似性是连续递归的自动机的状态数是固定的。
2019-01-22 cs.FL cs.LO
Pushdown Automata and Context-Free Grammars in Bisimulation Semantics
本文在反应式图灵机及互模拟语义下，通过引入带中间接受的序列算子与状态感知概念，恢复了下推自动机与上下文无关文法之间的经典对应关系。
2023-03-01 cs.FL cs.LO
Equivalence Checking and Intersection of Deterministic Timed Finite State Machines
人们对定义具有丰富时间的自动机模型越来越感兴趣，例如用时钟扩展的有限自动机（时间自动机）。在本文中，我们研究确定性时间有限状态机（TFSM），即，有限状态机具有单个时钟、定时保护和超时，其将定时输入字转换为定时输出字。我们解决了等价性检查的问题，通过定义一个互模拟定时FSM的untimed的，反之亦然。此外，我们应用这些互模拟关系来建立两个定时有限状态机的交集，通过对它们进行反定时，相交并转换回定时交集。
2021-03-08 cs.FL
Witnesses and Counterexamples for Timed Bisimulation
TU Darmstadt（达姆施塔特工业大学）；University of Siegen（锡根大学）
针对时间自动机互模拟验证，提出基于虚拟时钟扩展区域图的方法，既能有效检查时间互模拟等价，又能生成有效见证或反例解释行为差异。
2026-06-16 cs.FL cs.LO
Bisimulation Equivalence of First-Order Grammars
本文给出了一阶文法（重写一阶项根的标号规则的有限集合）互模拟等价性的可判定性证明。该等价性推广了DPDA（deterministic pushdown automata）等价性，其结果与Senizergues（1998，2005）在方程图框架下的结果或在PDA框架下的结果一致.经典一阶项的框架似乎特别有用，可以为更广泛的受众提供可以理解的证明。我们还讨论了Fu和Yin（2014）宣布的分支双相似性的扩展。
2014-05-30 cs.FL cs.LO
Equivalence of pushdown automata via first-order grammars
给出了一阶文法互模拟等价的可判定性证明。它是Sénizergues（1998，2005）的一个结果的另一种证明，该结果包含了他对确定性下推自动机的著名可判定性问题的肯定解。所提出的证明是概念上更简单，一个特别的新颖性是，它不是作为两个半决策程序，但它提供了一个明确的算法，可能是服从复杂性分析。
2020-08-17 cs.FL cs.LO
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
Computing Distances between Probabilistic Automata
我们提出了概率自动机（PA）上的模拟和互模拟的宽松概念，允许一些误差epsilon。当λ为零时，我们恢复PA上的互模拟和模拟的通常概念。我们给出了这些概念的逻辑特征，通过选择适当的逻辑，它不同于基本的，L与否定和L没有否定，由模态算子。使用流网络，我们展示了如何计算PTIME中的关系。这允许定义PA的状态之间的有效可计算的非折扣距离。引入了对该距离的自然修改，以获得折扣距离，从而削弱了长期转换的影响。我们比较我们的概念的距离，以前定义的其他人，并说明我们的方法上的各种例子。我们还表明，我们的距离是不膨胀的过程代数算子。虽然没有否定的L是一个合适的逻辑，以确定性PA的双（双）模拟，它不是一般的PA;有趣的是，我们证明，它确实是一个较弱的概念，称为先验双（双）模拟，我们证明是NP-难以决定。
2011-07-06 cs.FL cs.LO
Note on Undecidability of Bisimilarity for Second-Order Pushdown Processes
Broadbent和Göller（FSTTCS 2012）证明了无ε二阶下推自动机生成的过程的互模拟等价性的不可判定性。我们添加了一些关于所使用的证明技术的注释，称为Defender's forcing，以及具有ε转换的一阶下推自动机的相关不可判定性证明（Jančar and Srba，JACM 2008）。
2013-03-04 cs.FL cs.LO
Bisimulation equivalence of first-order grammars is Ackermann-hard
一阶文法的互模拟等价（或互相似性）是可判定的，正如Senizergues（1998，2005）的可判定性结果所示，该结果在有限出度的方程图或仅具有确定性和弹出ε-转换的下推自动机（PDA）的等价框架中给出。Benedikt、Goeller、Kiefer和Murawski（2013）已经证明，没有ε跃迁的PDA（偶）的双相似性问题是非初等的。在这里，我们显示阿克曼硬度双相似的一阶文法。语法不使用显式的ε-转换，但它们对应于上述PDA与（确定性和弹出）ε-转换，这个功能是实质性的下界证明。这个证明是基于重置（或有损）计数器机器的可达性问题的（多项式）归约，Schnoebelen（2010）已经证明了阿克曼硬度;事实上，这个可达性问题在Schmitz（2013）定义的快速增长复杂性类的层次中是阿克曼完全的。
2013-12-13 cs.FL cs.LO
Bisimilarity in fresh-register automata
本文研究寄存器自动机和新鲜寄存器自动机的互模拟问题复杂度，证明通用情况为EXPTIME完全，无重复值情况可利用对称性降为PSPACE/NP，填补语言等价性复杂度空白并反驳旧猜想，还发现下推存储会使互模拟不可判定。
2025-02-05 cs.FL cs.LO
Presheaf automata
本文提出预层自动机作为高维自动机等形式化方法的推广，发展了其语言理论基础并定义开映射扩展模拟与互模拟，证明了有限型预层自动机包含所有 Petri 网，且存在不满足 Kleene 定理的子类。
2025-08-15 cs.FL math.CT
Checking Timed Bisimilarity with Virtual Clocks
Technical University of Darmstadt（达姆施塔特工业大学）；University of Siegen（锡根大学）；Accso – Accelerated Solutions GmbH（Accso-加速解决方案有限公司）
本文提出了一种扩展区图的虚拟时钟表示法，用于解决定时自动机的双射性检查问题，该方法在平均情况下比区域图更小，并通过实验验证了其有效性。
2026-08-31 cs.FL
Checking Timed Bisimulation with Bounded Zone-History Graphs -- Technical Report
时间自动机（TA）是一个行之有效的形式化描述离散状态/连续时间行为的时间临界反应系统。关于基本分析问题的候选人的实现对规范进行比较，都给定为TA，它已被证明，定时跟踪等价是不可判定的，而定时互模拟等价是可判定的。相应的证明利用区域图，一个有限的，但通常非常占用空间的TA语义表征。因此，大多数实用的TA工具利用区域图，而不是符号和一般更有效的表示TA语义，自动化分析任务。然而，区域图只产生声音的分析任务的结果被简化为平原可达性问题，从而检查定时双相似性太不精确。在本文中，我们提出了有界区域历史图，一种新的表征TA语义促进可调的权衡精度和可扩展性之间的时间双相似性检查。据我们所知，我们的工具TimBrCheck是目前唯一可用的工具，用于有效地检查定时双相似性，甚至支持无声移动的非确定性TA。我们进一步提出了实验结果，从应用我们的工具收集的社区基准，提供洞察精度和效率之间的权衡，取决于绑定值。
2020-09-16 cs.FL cs.LO
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
Coherent Minimisation: Towards efficient tamper-proof compilation
自动机表示程序的游戏语义模型，其目的是在输入输出行为受游戏规则约束的环境中运行。这可能导致状态之间等价的概念，这比传统的互模拟概念弱，因为不是所有的动作都可用于环境。一个试图破坏游戏规则的环境实际上是对一个系统进行低级攻击。在本文中，我们将展示如何（以及为什么）在基于游戏的硬件合成中执行游戏规则，以及如何使用这种较弱的等价概念（称为相干等价）来积极地最小化自动机。
2012-12-17 cs.FL cs.LO cs.PL
Deciding semantic finiteness of pushdown processes and first-order grammars w.r.t. bisimulation equivalence
如果一个给定的配置的下推自动机（PDA）是双相似的一些（未指定）有限状态过程的问题是可判定的。的可判定性证明的框架中的一阶文法，这是由有限的标签规则，重写根的一阶项。该框架相当于PDA，其中也允许确定性（即无选择性）ε-步骤，即Sénizergues展示了一个决定双相似性的复杂过程（1998，2005）的模型。这样的过程在这里被用作算法的黑盒部分。这一结果扩展了Stearns（1967）提出的确定性PDA的正则性问题的可判定性，后来Valiant（1975）在复杂性方面进行了改进。非确定性PDA的可判定性问题，在这里得到了肯定的回答，一直是开放的（如所指出的，例如，作者：Broadbent和Göller，2012年）。
2019-09-23 cs.FL cs.LO
Timed I/O Automata: It is never too late to complete your timed specification theory
本文提出基于 Timed I/O Automata 与 Timed I/O Transition Systems 的完整实时系统规范理论，涵盖精化、一致性、组合、商等构造，并由严格证明和 ECDAR 工具实现支持。
2023-07-13 cs.FL cs.SE
An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata
在80年代中期，Lichelman，Pnueli和Zuck证明了一个经典定理，说明Past LTL的每个公式（带有过去算子的LTL的扩展）都等价于$\bigwedge_{i=1}^n \mathbf{G}\mathbf{F} φ_i \vee \mathbf{F}\mathbf{G} ψ_i$形式的公式，其中$φ_i$和$ψ_i$只包含过去算子。几年后，Chang、Manna和Pnueli在这个结果的基础上导出了LTL的类似范式。这两个规范化过程都有一个非初等的最坏情况爆破，并遵循从公式到无计数器自动机到无星正则表达式再回到公式的相关路径。我们在这两点上都有所改进。我们提出了一个直接的和纯粹的语法规范化程序LTL产生一个范式，相当于一个由张，曼纳，和Pnueli，只有一个单一的指数爆破。作为一个应用，我们推导出一个简单的算法，将LTL转换成确定性的拉宾自动机。该算法规范化的公式，将其转换成一个特殊的非常弱的交替自动机，并适用于一个简单的determinisation程序，有效的只有这些特殊的自动机。
2020-05-01 cs.FL cs.LO
