模糊自动机之间的深度有界模糊模拟与互模拟

模糊自动机之间最大模拟和互模拟的计算算法

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-25cs.AIcs.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-05cs.AIcs.FL

概率自动机中等价与互模拟何时结合

When Equivalence and Bisimulation Join Forces in Probabilistic Automata

概率自动机是拉宾在1963年作为语言接受者引入的。两个自动机是等价的，当且仅当它们以相同的概率接受每个单词。另一方面，在过程代数领域，Segala于1995年重新提出了概率自动机，它比Rabin的自动机更具有一般性。互模拟已经提出了Segala的自动机来表征它们之间的等价性。到目前为止，等价的两个概念及其特征是最独立的研究。在本文中，我们考虑Segala的自动机，并提出了一个新的概念，基于分布的互模拟加入现有的等价和双相似。我们的互模拟桥梁社区中的两个密切相关的概念，并提供了一个统一的方式来研究他们的特点。我们通过研究基于分布的互模拟度量证明了我们的定义的实用性，这产生了拉宾自动机的等价性的强大概念。

2014-03-08cs.FLcs.LO

马尔可夫自动机：利用非自然消失状态判定弱互模拟

Markov Automata: Deciding Weak Bisimulation by means of non-naively Vanishing States

提出了一种基于马尔可夫自动机的弱互模拟判定算法。为此，定义了消失状态的不同概念（从广义随机Petri网领域已知的概念）。消失状态是必不可少的相关概念（基于状态）天真的弱互模拟和（基于分布）弱互模拟。本文提出的互模拟算法遵循划分-细化方案，具有指数时间复杂度。

2014-04-30cs.FLcs.LO

用跟随自动机实现模糊正则表达式到模糊自动机的变形

Metamorphosis of Fuzzy Regular Expressions to Fuzzy Automata using the Follow Automata

为了处理系统的不确定性，有限自动机被推广为模糊自动机。Stamenkovic和Ciric提出了一种使用位置自动机从模糊正则表达式构造模糊自动机的方法。从正则表达式构造有限自动机的方法有很多种，如Thompson构造法、Antimirov偏导数法、Glushkov自动机和跟随自动机等。本文提出了一种利用跟随自动机的概念将模糊正则表达式转换为模糊自动机的方法。使用所提出的方法得到的模糊自动机的状态数是小于现有的方法在文献中。

2014-12-01cs.FL

概率自动机的保代价互模拟

Cost Preserving Bisimulations for Probabilistic Automata

概率自动机构成了并发概率系统的通用和优雅的模型。他们配备了一个组合理论支持抽象，使弱概率互模拟作为参考概念，总结抽象的效果。本文考虑了增加成本的概率自动机。它扩展了概率自动机中弱转换的概念，使得沿着弱转换产生的成本被捕获。这就产生了成本保持和成本约束的变化弱概率双相似性，我们建立组合属性相对于并行组合。此外，多项式时间的决策算法，提出了，可以有效地用于计算马尔可夫决策过程中的组合方式的回报约束抽象。

2015-02-16cs.FLcs.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-11cs.FLcs.LO

模糊自动机的Brzozowski型判定

Brzozowski type determinization for fuzzy automata

在本文中，我们适应著名的Brzozowski确定方法的模糊自动机。该方法给出了比所有先前已知的用于确定模糊自动机的方法更好的结果，所述模糊自动机是由Berglohlávek [Inform Sciences 143（2002）205- 209]，Li和Pedrycz [Fuzzy Set Syst 156（2005）68- 92]，Ljatović等人[Inform Sciences 178（2008）164- 180]开发的，和Jančić等人[Inform Sciences 181（2011）1358- 1368]。也就是说，在普通的非确定性自动机的情况下，Brzozowski型确定的模糊自动机的结果在一个最小的清晰的确定性模糊自动机相当于开始模糊自动机，我们表明，有情况下，当所有以前的方法导致无限自动机，而Brzozowski型确定的结果在有限的。本文讨论了完全剩余格上的模糊自动机，但在更一般的情况下，对于格序幺半群上的模糊自动机，甚至对于交换半环上的加权自动机，也可以得到相同的结果。

2014-02-08cs.FL

模糊自动机极小化的可判定性

Decidability of minimization of fuzzy automata

状态最小化是自动机理论中的一个基本问题。该问题在模糊自动机的研究中也具有重要意义。然而，大多数文献只考虑模糊自动机的状态约简，而模糊自动机的状态最小化问题几乎没有涉及。因此，在本文中，我们专注于后一个问题。形式上，模糊自动机极小化问题的判定形式如下：\begin{itemize} \item Given a fuzzy automaton $\mathcal{A}$ and a natural number $k$, that is, a pair $\langle \mathcal{A}, k\rangle$, is there a $k$-state fuzzy automaton equivalent to $\mathcal{A}$? \end{itemize}我们首次证明了全序格上模糊自动机的上述问题是可判定的。为此，我们首先给出了模糊多项式方程组的概念，然后提出了一个程序来解决这些系统。然后，我们将模糊多项式方程组的可解性应用于上述极小化问题，得到了可判定性。最后，我们指出，上述问题至少是PSAPCE-完全一样难。

2013-05-18cs.FL

有向模糊不确定自动机

Directable Fuzzy and Nondeterministic Automata

我们研究了三个概念的模糊自动机的D1-，D2-和D3-不确定自动机的方向性。因此，模糊自动机的输入字$w$是D1-定向的，如果一个固定的单一状态可由$w$从所有状态到达，D2-定向的，如果完全相同的状态可由$w$从每个状态到达，和D3-定向的，如果有一个状态可由$w$从每个状态到达。我们研究了模糊自动机的各种定向词集，证明了其定向性质是可判定的，并展示了如何从定向非确定自动机理论推导出这样的结果。此外，我们建立了不同类别的有向模糊自动机在形成子自动机、同态像和有限直积类操作下的闭包性质。

2017-09-22cs.FL

分配格上的模糊交替$\mathrm{B\ddot{u}chi}$自动机

Fuzzy alternating $\mathrm{B\ddot{u}chi}$ automata over distributive lattices

给出了一种新的分配格上的模糊交替$\mathrm{B\ddot{u}chi}$自动机：权值放在运行树的每个叶节点上，而不是放在从每个节点到其子节点的边上。这样的设置对于只需要进行对偶运算，将每个最终权值替换为它的补码就可以得到补码是非常有利的。证明了$L$ -模糊非确定$\mathrm{B\ddot{u}chi}$自动机与$L$ -模糊交替$\mathrm{B\ddot{u}chi}$自动机具有相同的表达能力.给出了一种直接构造方法（不需要$L$ -模糊非确定$\mathrm{B\ddot{u}chi}$的相关知识，如上述等价关系及其闭包性质），证明了$L$ -模糊交替共$\mathrm{B\ddot{u}chi}$自动机所识别的语言也是$L$ -模糊$ω$ -正则的.此外，本文还讨论了模糊交替$\mathrm{B\ddot{u}chi}$自动机的闭包性质和决策问题。

2016-03-15cs.FL

Wheeler 双射

Wheeler Bisimulations

University of Helsinki（赫尔辛基大学）

本文研究了双射与数据压缩的关系，提出Wheeler双射概念，展示如何通过线性时间构建最小Wheeler NFA，改进了传统双射方法。

2026-06-29cs.DScs.FL

模糊确定自顶向下树自动机

Fuzzy Deterministic Top-down Tree Automata

本文介绍并研究了格L上的模糊确定自顶向下树自动机。被这些自动机识别的L-fuzzy树语言被称为DT-可识别的，并且它们形成了所有正则L-fuzzy树语言的$Rec_L$族的真子集$DRec_L$。我们证明了一个泵引理$DRec_L$从几个可判定性的结果如下。建立了$DRec_L$在各种操作下的封闭性。我们还用L-fuzzy路径语言刻画了DT-可识别性，证明了正则L-fuzzy树语言的路径闭包是DT-可识别的，正则L-fuzzy树语言是否是DT-可识别的是可判定的.在大多数的文章中，L只是任何非平凡的有界格，但有时它被假定为分配的，甚至是一个有界链。

2019-11-26cs.FL

保持互模拟的时间自动机时钟约简

Reducing Clocks in Timed Automata while Preserving Bisimulation

随着时钟数目的增加，模型检验时间自动机变得越来越复杂。因此，人们希望用尽可能少的时钟来构造一个自动机。检查是否存在一个具有较少时钟的时间自动机，使得原始自动机接受的时间语言被保留的问题是不可判定的。在本文中，我们给出了一个结构，它对任何给定的时间自动机产生一个时间双相似自动机与最少数量的时钟。此外，我们表明，这样一个自动机的最小可能数量的时钟可以构建的时间是双指数的原始自动机的时钟的数量。

2015-05-20cs.FLcs.LO

半环上加权自动机互模拟的余代数

Coalgebras for Bisimulation of Weighted Automata over Semirings

本文在半模和集合范畴的余代数框架下研究加权自动机，证明最终余代数分别刻画加权语言等价与加权互模拟，并推广了线性关系概念，提出前向划分细化算法及终止条件。

2023-01-13cs.FLcs.LO

由模糊正则表达式构造模糊自动机

Construction of fuzzy automata from fuzzy regular expressions

Li和Pedrycz [Y. M. Li，W. Pedrycz，Fuzzy finite automata and fuzzy regular expressions with membership values in lattice-ordered monoid，Fuzzy Sets and Systems 156（2005）68- 92]已经证明了基本结果，这些结果提供了在格序monoid中表示具有隶属值的模糊语言的不同等价方式，并且推广了形式语言的经典理论的众所周知的结果。特别是，他们已经证明，一个模糊语言的整体格序幺半群可以表示为模糊正则表达式，当且仅当它可以识别的模糊有限自动机。然而，他们没有给出任何有效的方法来构造一个等价的模糊有限自动机从一个给定的模糊正则表达式。在本文中，我们提供了这样一个有效的方法。通过将模糊正则表达式α中的标量变换为新的扩展字母表中的字母，将模糊正则表达式α转化为普通正则表达式α R。然后，从识别语言的任意非确定性有限自动机A开始，||α_R||用正则表达式α R表示，构造了模糊有限自动机A_α和A_α^r，它们的状态数与自动机A相同或更少，它们识别模糊语言||α||由模糊正则表达式α表示。起始的非确定性有限自动机A可以从α_R中使用任何一种众所周知的将正则表达式转换为非确定性有限自动机的构造来获得，例如Glushkov-McNaughton-Y…

2011-05-31cs.FL

模糊有限自动机判定方法的进一步改进

Further improvements of determinization methods for fuzzy finite automata

在本文中，我们结合确定性和状态约简的方法到两个在一个算法，同时执行确定性和状态约简。这些算法比Belohlavek [Inform Sciences 143（2002）205-209]，Li和Pedrycz [Fuzzy Set Syst 156（2005）68-92]，Lidjatović等人[Inform Sciences 178（2008）164-180]开发的模糊有限自动机的所有先前确定算法表现更好，和Jančić et al. [Inform Sciences 181（2011）1358-1368]，在这个意义上，它们产生更小的自动机，而需要相同的计算时间。唯一的例外是最近由Jančić和Jenirić [Fuzzy Set Syst（2014），to appear]开发的Brzozowski类型确定算法，它产生一个最小的清晰确定性模糊自动机，但这里创建的算法也可以在Brzozowski类型算法中使用并提高其性能。

2014-12-07cs.FL

非确定分支余代数的自由开态射的路范畴

Path category for free - Open morphisms from coalgebras with non-deterministic branching

对于过渡系统的变分及其互模拟有不同的分类方法。一类是函子G的余代数，其中互模拟定义为G-余代数同态的一个跨距。另一个是在路径范畴和开态射方面，其中互模拟被定义为开态射的跨度。这种相似性不是巧合：给定一个函子G，满足一定的条件，我们导出了点G-余代数和松弛同态的路范畴，使得开态射恰好是G-余代数同态。上述构造为不同类型的变迁系统免费提供了路径范畴和迹语义：（1）非确定性树自动机（2）正则非确定性名义自动机（RNA），一种生活在名义集合中的表达自动机概念（3）多分类变迁系统。这最后一个例子与拉索塔的结构有关，它是在相反的方向上。

2019-02-15cs.FL

模糊自动机的语言包含度判定

Determinization of fuzzy automata by means of the degrees of language inclusion

模糊有限自动机的确定性在这里被理解为将它们转换为等价的清晰确定性模糊自动机的过程，该模糊自动机可以被视为具有可能无限多个状态的确定性，但是具有终端状态的模糊集。特别重要的确定性方法是那些提供一个最小的清晰的确定性模糊自动机相当于原来的模糊有限自动机，称为规范化方法。模糊有限自动机的一种规范化方法，Brzozowski型确定化，最近由Jančić和Jenirić在[10]中发展。在这里，我们提供了另一个规范化方法的模糊有限自动机$\cal A=(A,σ, δ,τ)$在一个完整的剩余格$\cal L$，基于包含度的正确的模糊语言与状态的$\cal A$到左导数的模糊语言识别的$\cal A$。所提出的过程终止于一个有限数目的步骤时，$δ$，$σ$和$τ$采取的成员值生成一个有限的子半环的半环约简的$\cal L$。该过程通常比Brzozowski型确定快，并且如果剩余格$\cal L$中的基本操作可以在恒定时间内执行，则其具有与[8]，[11]，[12]中提供的所有其他确定过程相同的计算时间。

2014-12-15cs.FL

一阶文法的互模拟等价是ACKERMANN-完全的

Bisimulation Equivalence of First-Order Grammars is ACKERMANN-Complete

Sénizergues（1998，2005）证明了两个具有限制静默动作的下推自动机是否弱双相似。我们提供了第一个已知的复杂性上界这个著名的问题，在等效设置的一阶文法。这ACKERMANN上限是最佳的，我们还表明，强双相似性是连续递归的自动机的状态数是固定的。

2019-01-22cs.FLcs.LO

下推自动机与上下文无关文法在互模拟语义中的对应关系

Pushdown Automata and Context-Free Grammars in Bisimulation Semantics

本文在反应式图灵机及互模拟语义下，通过引入带中间接受的序列算子与状态感知概念，恢复了下推自动机与上下文无关文法之间的经典对应关系。

2023-03-01cs.FLcs.LO

模糊自动机在余格上的软状态约简

Soft state reduction of fuzzy automata over residuated lattices

本文提出软状态约简方法，通过近似不变性在余格上减少模糊自动机状态，提升计算效率。

2025-12-07cs.FL

模糊有限自动机的近似状态约简

Approximate State Reduction of Fuzzy Finite Automata

本文提出模糊有限自动机的近似状态约简，要求约简后与原自动机在有限长度词上行为匹配，并给出四种约简方法。

2023-09-06cs.FL

确定性时间有限状态机的等价性检验与相交性

Equivalence Checking and Intersection of Deterministic Timed Finite State Machines

人们对定义具有丰富时间的自动机模型越来越感兴趣，例如用时钟扩展的有限自动机（时间自动机）。在本文中，我们研究确定性时间有限状态机（TFSM），即，有限状态机具有单个时钟、定时保护和超时，其将定时输入字转换为定时输出字。我们解决了等价性检查的问题，通过定义一个互模拟定时FSM的untimed的，反之亦然。此外，我们应用这些互模拟关系来建立两个定时有限状态机的交集，通过对它们进行反定时，相交并转换回定时交集。

2021-03-08cs.FL

典型犹豫模糊语言与自动机

On Typical Hesitant Fuzzy Languages and Automata

Universidade Federal do Vale do São Francisco（圣弗朗西斯科河谷联邦大学）；Universidade Federal do Rio Grande do Norte（北大河州联邦大学）

不确定典型犹豫模糊自动机的思想是Costa和Bedregal提出的模糊自动机的推广。本文给出了一个典型的犹豫模糊语言可由非确定的典型犹豫模糊自动机计算的充要条件。此外，本文还引入了一类新的具有清晰转换的典型犹豫模糊自动机，并证明了这类新的模糊自动机与Costa和Bedregal提出的模糊自动机是等价的

2021-02-18cs.CLcs.FL

模糊有限自动机的有向词

Directing Words of Fuzzy Finite Automata

一个确定的有限自动机是可定向的，如果它有一个引导字，把自动机从每一个状态带到同一个状态。这些概念也被扩展到其他类型的自动机。因此，B.~ Imreh和M.~ Steinby（1999）为非确定性有限自动机（NFA）确定了三种自然类型的定向词，称为D1-、D2-和D3-定向词。在这里，我们适应这些概念的模糊有限自动机（FFAs）。这样得到的D3指向词正是V.~引入的指向词。Karthikeyan和M. Rajasekar（2015年）。对于任何FFA F，我们关联一个NFA Fnd，它具有与F相同的定向词。因此，如果使用这些定义，直接FFA的理论简化为NFA的理论。我们还引入了三种新的模糊自动机导向词，我们分别称之为DD 1-，DD 2-和DD 3-导向词，它们更多地依赖于状态之间的模糊转移度。我们建立了任何给定FFA F的DDi指向词集合$DDi(F)$的一些基本性质。特别是，它表明，这些语言是定期的，DDi定向性是可判定的。对于所谓的正规FFA，语言DDi（F）具有一些特殊的性质。给出了DDi指向词的对应集合DDi（F）族之间的几种关系。我们还确定了各类DDi-有向自由场函数和正规自由场函数的完备交半格及其交。

2021-03-01cs.FL

MK-模糊自动机与MSO逻辑

MK-fuzzy Automata and MSO Logics

本文引入了与McCarthy-Kleene逻辑模糊化有关的双整数K上的MK-模糊自动机。我们的自动机的灵感，并打算作出贡献，在一个项目的运行时网络监控谓词逻辑的基础上正在开发的实际应用程序。我们调查的类可识别的MK-模糊语言接受的MK-模糊自动机，以及确定性可识别的MK-模糊语言接受其确定性的同行的封闭性。此外，我们建立了可识别的MK-模糊语言的Nivat样结果。我们引入了一个MK-模糊MSO逻辑，并证明了这个逻辑的一个片段与MK-模糊自动机的表达等价性，即，Büchi型定理

2017-09-07cs.FLcs.LO

时间互模拟的见证与反例

Witnesses and Counterexamples for Timed Bisimulation

TU Darmstadt（达姆施塔特工业大学）；University of Siegen（锡根大学）

针对时间自动机互模拟验证，提出基于虚拟时钟扩展区域图的方法，既能有效检查时间互模拟等价，又能生成有效见证或反例解释行为差异。

2026-06-16cs.FLcs.LO

模糊自动机的模糊拟序约简

Reduction of fuzzy automata by means of fuzzy quasi-orders

Faculty of Sciences and Mathematics, University of Niš（尼什大学科学与数学学院）

在我们最近的论文中，我们已经建立了一个模糊识别器的状态约简和一个特定的模糊关系方程系统的分辨率之间的密切关系。在这篇论文中，我们还研究了通过这些解决方案，这是模糊等价的减少。在本文中，我们将看到，在某些情况下，可以得到更好的减少使用该系统的解决方案，是模糊的准秩序。一般来说，模糊准秩序和模糊等价同样好的状态约简，但我们表明，右和左不变的模糊准秩序比右和左不变的模糊等价更好的减少。我们还表明，交替减少模糊准订单的方式比交替减少模糊等价的方式得到更好的结果。此外，我们研究了更一般类型的模糊准序，弱右和左不变的，我们表明，他们是密切相关的确定性的模糊识别器。我们还展示了弱左不变模糊拟序在模糊离散事件系统冲突分析中的一些应用。

2011-02-26cs.AIcs.FL

下推自动机的一阶文法等价性

Equivalence of pushdown automata via first-order grammars

给出了一阶文法互模拟等价的可判定性证明。它是Sénizergues（1998，2005）的一个结果的另一种证明，该结果包含了他对确定性下推自动机的著名可判定性问题的肯定解。所提出的证明是概念上更简单，一个特别的新颖性是，它不是作为两个半决策程序，但它提供了一个明确的算法，可能是服从复杂性分析。

2020-08-17cs.FLcs.LO

概率自动机之间距离的计算

Computing Distances between Probabilistic Automata

我们提出了概率自动机（PA）上的模拟和互模拟的宽松概念，允许一些误差epsilon。当λ为零时，我们恢复PA上的互模拟和模拟的通常概念。我们给出了这些概念的逻辑特征，通过选择适当的逻辑，它不同于基本的，L与否定和L没有否定，由模态算子。使用流网络，我们展示了如何计算PTIME中的关系。这允许定义PA的状态之间的有效可计算的非折扣距离。引入了对该距离的自然修改，以获得折扣距离，从而削弱了长期转换的影响。我们比较我们的概念的距离，以前定义的其他人，并说明我们的方法上的各种例子。我们还表明，我们的距离是不膨胀的过程代数算子。虽然没有否定的L是一个合适的逻辑，以确定性PA的双（双）模拟，它不是一般的PA;有趣的是，我们证明，它确实是一个较弱的概念，称为先验双（双）模拟，我们证明是NP-难以决定。

2011-07-06cs.FLcs.LO

用有界区域历史图检验时间互模拟--技术报告

Checking Timed Bisimulation with Bounded Zone-History Graphs -- Technical Report

时间自动机（TA）是一个行之有效的形式化描述离散状态/连续时间行为的时间临界反应系统。关于基本分析问题的候选人的实现对规范进行比较，都给定为TA，它已被证明，定时跟踪等价是不可判定的，而定时互模拟等价是可判定的。相应的证明利用区域图，一个有限的，但通常非常占用空间的TA语义表征。因此，大多数实用的TA工具利用区域图，而不是符号和一般更有效的表示TA语义，自动化分析任务。然而，区域图只产生声音的分析任务的结果被简化为平原可达性问题，从而检查定时双相似性太不精确。在本文中，我们提出了有界区域历史图，一种新的表征TA语义促进可调的权衡精度和可扩展性之间的时间双相似性检查。据我们所知，我们的工具TimBrCheck是目前唯一可用的工具，用于有效地检查定时双相似性，甚至支持无声移动的非确定性TA。我们进一步提出了实验结果，从应用我们的工具收集的社区基准，提供洞察精度和效率之间的权衡，取决于绑定值。

2020-09-16cs.FLcs.LO

时间自动机关系判定的统一方法及其博弈刻画

A Unifying Approach to Decide Relations for Timed Automata and their Game Characterization

在本文中，我们提出了一个统一的方法来决定各种互模拟，模拟等价和两个时间自动机状态之间的前序。我们提出了一个区域为基础的方法来决定这些关系，我们消除了显式的产品建设的区域图或区域图在经典的方法。我们的方法也是通用的，可以用来决定几个时间关系。我们还提出了一个游戏表征这些时间的关系，并表明，游戏层次结构反映了层次结构的时间关系。人们可以得到一个无限的游戏层次，因此游戏表征进一步表明，尚未研究的定义新的时间关系的可能性。游戏的特征也帮助我们提出一个公式，它编码两个状态之间的分离，不是定时bisimilarily。这样的区别公式也可以产生许多关系以外的时间双相似性。

2013-07-29cs.FLcs.LO