Rooted branching bisimulation as a congruence for probabilistic transition systems
我们提出了一个概率转换系统规范格式，被称为概率RBB安全，根分支互模拟是一个同余。同余定理是基于Fokkink的定性情况下的方法。要做到这一点，需要扩展标记转换系统设置中的转换系统规范理论，以处理句法和语义上的概率分布。我们提供了一个无干扰的表征的概率分支互模拟适应Andova等人的工作。交替模型。给出反例来证明格式所需的各种条件。
2015-09-29 cs.LO
A New Branching Bisimulation for Probabilistic Processes
College of Computer and Information Science, Southwest University（西南大学计算机与信息科学学院）；Hunan University of Arts and Science（湖南文理学院）；Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；School of Mathematics and Statistics, Hubei Minzu University（湖北民族大学数学与统计学院）
该研究为概率过程引入新分支双模拟，此双模拟诱导出更精细等价关系，其有根版本对含递归等构造的概率过程语言是同余关系，是一种新的等价关系定义。
2026-07-21 cs.LO
Compositional bisimulation metric reasoning with Probabilistic Process Calculi
我们研究的概率过程演算的标准运营商允许组合推理互模拟度量语义。我们认为，一致的连续性（概括了先前提出的非扩展性的属性）抓住了组合推理的本质，现在还允许组合推理递归过程。我们刻画了由标准过程代数算子组成的概率过程之间的距离。结合这些结果，我们演示了如何组合推理系统指定的连续进程代数运算符允许度量假设保证性能验证。
2016-12-30 cs.LO
Enabling Preserving Bisimulation Equivalence
大多数用于验证活性属性的公平性假设都被批评为过于强大或不切实际。另一方面，公正性，可以说是验证活性属性所需的最小公平性假设，并不被经典的语义等价所保留，例如强双相似性。为了克服这一缺陷，我们引入了一个更好的替代强双相似性，使保持双相似性。我们证明了这个等价是正义的保持和所有的标准运营商，包括并行组合的一个同余。
2021-07-31 cs.LO
Compositional equivalences based on Open pNets
建立程序或系统之间的等价关系对于验证程序的正确性（通过建立两个实现是等价的）和证明优化和程序转换（通过建立修改后的程序与源程序等价）都是至关重要的。程序存在几种等价关系，互模拟是这些等价关系中最通用的。在互模拟关系中，我们可以区分强互模拟和弱互模拟，强互模拟要求程序的每个动作都由等价程序的单个动作模拟，弱互模拟是一种粗糙的关系，允许某些动作是不可见的或内部移动的，因此不被等价程序模拟。pNet是对开放系统进行建模的自动机的概括。它们以变量和层次结构为特征。开放式pNet是具有洞的pNet，即层次结构内的占位符，稍后可以由子系统填充。本文定义了互模拟关系，用于比较指定为pNet的系统。我们首先定义了一个强互模拟开放pNet。然后，我们定义了一个类似于经典的弱互模拟的等价关系，并研究了它的性质。在这些性质中，我们感兴趣的是组合性：如果两个系统被证明是等价的，那么它们将无法通过它们的上下文来区分，并且当它们的洞被等价系统填充时，它们也将无法区分。我们确定充分条件的自动机，以确保组合的强和弱互模拟。文章用一个传输协议运行的例子来说明，它显示了我们的形式主义和我们的互模拟关系的特点。
2021-10-22 cs.LO
Coalgebraic Weak Bisimulation from Recursive Equations over Monads
标记转移系统的强互模拟是进程代数中最基本的等价之一，并且已经被推广到许多具有更丰富转移行为的系统。几乎所有随后的概念都是更一般的共代数互模拟概念的实例。然而，弱互模拟到目前为止还不太适合于共代数处理。在这里，我们试图关闭这一差距（参数化）弱等价，包括弱互模拟的共代数治疗。我们的分析要求函子定义的过渡类型的系统是基于一个合适的订单丰富的单子，这使我们能够捕捉弱等价的递归方程的最少不动点。我们的概念是在协议与现有的概念弱互模拟标记的过渡系统，概率和加权系统，简单的Segala系统。
2014-05-02 cs.LO
Bisimulations and Logical Characterizations on Continuous-time Markov Decision Processes
本文研究了连续时间马尔可夫决策过程（CTMDPs）的强互模拟等价和弱互模拟等价，以及这些关系在连续时间随机逻辑（CSL）中的逻辑刻画。对于强互模拟，它严格优于CSL等价。本文提出了CTMDPs的强和弱互模拟，并证明了对于CTMDPs的一个子类，强和弱互模拟分别关于CSL和不含next算子的CSL的子逻辑所诱导的等价性都是合理和完备的.然后，我们考虑了CSL的标准扩展，并表明它及其不含X的子逻辑可以分别通过任意CTMDP上的强和弱互模拟来完全表征。
2013-11-16 cs.LO
Bisimulations Meet PCTL Equivalences for Probabilistic Automata
概率自动机已成功地应用于并发和随机系统的形式化验证。有效的模型检验算法已经被研究，其中最常用的用于表达属性的逻辑是基于概率计算树逻辑（PCTL）及其扩展PCTL^*。提出了各种行为等价物，作为一个强大的工具，抽象和组合最小化的PA。不幸的是，这些等价是众所周知的合理的，但就PCTL或PCTL* 所诱导的逻辑等价而言并不完整。塞加拉在1995年指出了一个既健全又完整的行为等价的愿望，但多年来一直没有定论。在本文中，我们引入了新的概念，强互模拟关系，PCTL和PCTL* 的特点。我们扩展了弱互模拟的特点PCTL和PCTL* 没有下一个运营商，分别。此外，我们还扩展了模拟前序的框架。因此，我们的论文弥合了在这种情况下逻辑和行为等价性和前序之间的差距。
2013-06-21 cs.LO
A Logic with Reverse Modalities for History-preserving Bisimulations
我们引入事件标识符逻辑（EIL），它通过增加（1）反向和正向模态以及（2）跟踪事件的标识符来扩展Hennessy-Milner逻辑。我们表明，这种逻辑对应于遗传的历史保持（HH）互模拟等价在一个特定的真并发模型，即稳定的配置结构。此外，我们展示了如何自然子逻辑EIL对应于粗糙的等价。特别地，我们提供了弱历史保持（WH）和历史保持（H）互模拟的逻辑特征。据我们所知，以前已经给出了对应于HH和H互模拟的逻辑，但没有给出对应于WH互模拟的逻辑（当允许自动并发时）。我们还提出了特征公式，它描述了各个结构的历史保存等价。
2011-08-23 cs.LO
Logical Characterization of Bisimulation Metrics
互模拟度量为研究不确定性概率过程的行为提供了一种鲁棒而精确的方法。在本文中，我们提出了一个简单的概率变化的Hennessy-Milner逻辑的基础上的互模拟度量的逻辑表征。我们的方法是基于新的概念，模仿公式和公式之间的距离。前者是一个弱版本的著名的特征公式，并允许我们也（准备）概率模拟和概率双相似性的特点。后者是一个1-有界伪度量的公式，反映了Hausdorff和Kantorovich提升定义的双相似伪度量。我们证明了两个过程之间的距离等于它们自己的模仿公式之间的距离。
2016-10-26 cs.LO
Bisimulation of Labeled State-to-Function Transition Systems of Stochastic Process Languages
标号状态-函数转换系统，简称FuTS，允许一般半环上从状态到有限支集函数的多种转换方案。因此，他们构成了一个方便的建模工具来处理随机过程语言。本文提出了由FuTS引起的互模拟的概念，并证明了一个对应的结果，即FuTS-互模拟与相关函子的行为等价一致。作为一般的例子，具体的现有等价的核心的进程代数ACP，PEPA和IMC相关的互模拟特定的FuTS，提供通过对应的结果coalgebrical的理由，这些演算的等价。
2012-09-07 cs.LO
Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation
概率过程的许多行为等价或前序都涉及提升操作，该操作将状态关系转换为状态分布关系。我们表明，现有的几个建议，提升关系可以调和到本质上相同的提升操作的不同介绍。更有趣的是，这种提升操作很好地对应于康托洛维奇度量，这是数学中用于将状态度量提升为状态分布度量的基本概念，此外，提升操作与优化理论中的最大流问题有关。提升操作产生了一个整洁的概念，概率互模拟，我们提供逻辑，度量和算法特征。具体来说，我们扩展了Hennessy-Milner逻辑和模态μ演算与一个新的模态，从而在一个足够的概率双相似性和表达逻辑，分别。提升操作和Kantorovich度量的对应关系导致了互模拟作为伪度量的自然特征，伪度量是单调函数的后不动点。我们还提出了一个“在飞”算法来检查是否在有限系统中的两个状态相关的概率双相似性，利用提升操作和最大流问题之间的密切关系。
2011-03-23 cs.LO
Applicative Bisimulation and Quantum $λ$-Calculi (Long Version)
应用互模拟是一种在高阶函数式语言中检验程序等价性的共归纳技术。就上下文对等而言，它是合理的，有时是完整的。在本文中，我们表明，应用互模拟也工作时，底层语言的程序采取的形式的线性$λ$ -演算扩展的功能，如概率二进制选择，但也量子数据，后者是一个设置中的线性发挥作用。的主要结果是证明所获得的概念的双相似性的合理性。
2015-06-22 cs.LO
SOS rule formats for convex and abstract probabilistic bisimulations
$nt μfθ/ ntμxθ$格式的概率转换系统规范（PTSS）为Segala类型的系统提供结构操作语义，这些系统表现出概率和非确定性行为，并保证双相似性对于以这种格式定义的所有运算符都是一致的。从$nt μfθ/ ntμxθ$格式开始，我们得到限制格式，保证三个粗互模拟等价的同余。我们重点讨论了（i）Segala的互模拟变体，它考虑了组合转移，我们称之为“凸互模拟”;（ii）考虑Park & Milner的互模拟在通常的剥离概率转移系统上的互模拟等价性（翻译成一个标记的转换系统），我们在这里称之为“概率抹杀互模拟”;以及（iii）“概率抽象互模拟”，其与互模拟一样，保留分布的结构，但相反，其忽略概率值。此外，我们比较这些互模拟等价，并为他们每个人提供了一个逻辑表征。
2015-08-27 cs.LO cs.PL
Weak bisimulations for labelled transition systems weighted over semirings
带权标号的变迁系统是变迁被赋予从交换幺半群中抽取的权的LTS。WLTS是LTS的一个分支，提供了强（加权）互模拟的一般概念。在本文中，我们扩展到其他行为等价的框架，考虑半环的权重。利用这个额外的结构，我们介绍了一个一般的概念，弱加权互模拟。我们表明，弱加权互模拟与通常的弱互模拟的情况下，非确定性和全概率系统相吻合，而且，它自然地提供了一个定义的弱互模拟也为各种LTS，这个概念是目前失踪（如随机系统）。最后，我们提供了一个分类帐户的弱加权互模拟的共代数结构，这种结构指出了如何端口我们的方法，其他等价的基础上不同的概念的可观测性。
2013-10-15 cs.LO
Bisimulations for Nondeterministic Labeled Markov Processes
我们扩展了标记马尔可夫过程的理论与内部不确定性，一个基本概念，为进一步发展的过程理论与抽象的不确定性连续概率系统。我们定义了非确定性标记马尔可夫过程（NLMP），并提供了三个定义的互模拟：一个传统的表征，基于状态的互模拟定制我们的“可测量”的非确定性，和基于事件的互模拟。我们展示了它们之间的关系，包括最大状态互模拟也是事件互模拟。我们还介绍了变化的Hennessy-Milner逻辑事件互模拟的特点，这是健全的w.r.t.任意NLMP的其他互模拟。然而，这个逻辑是无限的，因为它包含一个可数的$\lor$。然后，我们引入了一个有限的子逻辑，其特征的图像有限NLMP的基本测量空间也是解析的所有互模拟。因此，在这种情况下，我们处理的所有互模拟概念都是相等的。最后，我们表明，所有的概念的互模拟是不同的，在一般情况下。将它们分开的反例变成非概率NLMP。
2010-11-15 cs.LO
When Equivalence and Bisimulation Join Forces in Probabilistic Automata
概率自动机是拉宾在1963年作为语言接受者引入的。两个自动机是等价的，当且仅当它们以相同的概率接受每个单词。另一方面，在过程代数领域，Segala于1995年重新提出了概率自动机，它比Rabin的自动机更具有一般性。互模拟已经提出了Segala的自动机来表征它们之间的等价性。到目前为止，等价的两个概念及其特征是最独立的研究。在本文中，我们考虑Segala的自动机，并提出了一个新的概念，基于分布的互模拟加入现有的等价和双相似。我们的互模拟桥梁社区中的两个密切相关的概念，并提供了一个统一的方式来研究他们的特点。我们通过研究基于分布的互模拟度量证明了我们的定义的实用性，这产生了拉宾自动机的等价性的强大概念。
2014-03-08 cs.FL cs.LO
Probabilistic Bisimulation for Parameterized Systems (Technical Report)
概率互模拟是概率系统过程等价的一个基本概念。其中，它有重要的应用，包括形式化的匿名性的几个通信协议。在有限系统的概率互模拟验证方面有大量的工作。然而，对于参数化系统，情况并非如此，其中问题通常是不可判定的。在本文中，我们提供了一个通用的框架推理概率互模拟参数化系统。我们的方法是在软件验证的精神，其中我们编码的概率互模拟的证明规则，并使用可判定的一阶理论来指定系统和候选互模拟关系，然后可以自动检查对证明规则。作为一个案例研究，我们表明，我们的框架是足够的表达证明匿名性的参数化用餐密码协议和参数化等级协议，当提供一个候选人经常互模拟关系。这两个协议迄今无法验证现有的自动方法。此外，在标准自动机学习算法的帮助下，我们证明了候选关系可以完全自动地合成，使得验证完全自动化。
2020-11-04 cs.LO cs.SE
Bisimulation Equivalence of First-Order Grammars
本文给出了一阶文法（重写一阶项根的标号规则的有限集合）互模拟等价性的可判定性证明。该等价性推广了DPDA（deterministic pushdown automata）等价性，其结果与Senizergues（1998，2005）在方程图框架下的结果或在PDA框架下的结果一致.经典一阶项的框架似乎特别有用，可以为更广泛的受众提供可以理解的证明。我们还讨论了Fu和Yin（2014）宣布的分支双相似性的扩展。
2014-05-30 cs.FL cs.LO
Behavioural equivalences for fluid stochastic Petri nets
我们提出流体等价比较和减少标记流体随机Petri网（LFSPNs）的行为，同时保持其离散和连续的属性。我们定义了一个线性时间关系的流体跟踪等价和它的分支时间对应，流体互模拟等价。这两种流体关系考虑到LFSPNs行为的基本特征：功能活动，随机定时和流体流动。我们考虑了连续标记对离散标记没有影响，离散部分是连续时间随机Petri网的LFSPN。LFSPN的离散部分的基础随机模型是连续时间马尔可夫链（CTMCs）。LFSPN的连续部分的性能分析是通过相关的随机流体模型（SFM）完成的。我们表明，流体迹等价保持平均潜在的流体变化量的过渡序列的每一个特定的长度。我们证明了流体互模拟等价性保留了聚集的概率函数：底层CTMC的静态概率质量，以及相关SFM的静态流体缓冲区空概率，流体密度和分布。因此，等价保证了一些离散和连续的性能指标的身份。流体互模拟等价，然后使用简化的定性和定量分析的LFSPN通过离散可达图和底层CTMC。为了描述与SFM相关的商，定义了概率函数的导数。基于Hennessy-Milner逻辑HML，我们用两种新的流体模态逻辑$HML_{flt}$和$HML_{flb}$刻画了逻辑上的流体迹和互模拟等价.以公文处理系统为例，通过流体互模拟等价性验证了行为分析方法。
2017-06-08 cs.LO
A Definition Scheme for Quantitative Bisimulation
FuTS，状态到功能转换系统是标记转换系统和熟悉的定量语义模型概念的推广，如连续时间马尔可夫链，交互式马尔可夫链和马尔可夫自动机。提出了一个与FuTS相关的强互模拟概念的定义的一般方案。它表明，这种概念的互模拟的FuTS相一致的行为等价的共代数概念的函子集的类型的FuTS。对于一系列具体的定量语义模型，证明了文献中所报道的互模拟概念与从该方案中得到的定量互模拟概念是一致的。比较包括具有正交行为的模型，如交互式马尔可夫链，以及具有多个行为级别的模型，如马尔可夫自动机。作为一个后果的一般结果有关的FuTS互模拟和行为等价，我们得到，在一个系统的方式，共代数的基础上讨论的所有定量互模拟。
2015-09-29 cs.LO
Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence
本文提出 PDNF 互模拟，利用无栈 LTS、调用栈即时饱和与 up-to 技术，使具有局部状态的高阶程序在无界栈和未知函数输入下仍可判定上下文等价性。
2023-11-02 cs.LO cs.PL
Simulations and Bisimulations For Coalgebraic Modal Logics
我们定义了一个概念的Lambda模拟的共代数模态逻辑，参数的选择Lambda的谓词提升函子T。我们证明了这个概念在几个方面是足够的：i）它保留了正公式的真值，ii）对于Lambda，单调谓词提升的分离集，Lambda-互模拟的相关概念对应于T-行为等价（此外Lambda-n-互模拟对应于T-n-行为等价），以及iii）事实上，对于Lambda-分离和T保持弱回调，双功能Lambda-互模拟是T-互模拟。从本质上讲，我们得到了一个模块化的等价概念，当与一组单独的单调谓词提升一起使用时，与T-行为等价一致，而不管T是否保留弱回调（与T-双相似性的概念不同）。
2013-04-11 cs.LO math.LO
Weak Markovian Bisimulation Congruences and Exact CTMC-Level Aggregations for Concurrent Processes
我们最近定义了一个弱马尔可夫互模拟等价的集成时间设置，它减少了序列的指数定时的内部行动，个人指数定时的内部行动具有相同的平均持续时间和执行概率的相应序列。这种弱马尔可夫互模拟等价是一个同余序列过程的抽象和原来诱导一个确切的CTMC级聚集在稳态所有考虑的过程。然而，它并不是平行合成的一致性。在本文中，我们展示了如何推广的等价性的方式，一个合理的权衡抽象，组合性和精确性之间实现了并发进程。我们将看到，通过增强并行计算中的抽象能力，可以检索关于并行组合的同余属性，所得到的CTMC级聚合仅对于所考虑过程的某个子集在稳定状态下是精确的。
2012-07-04 cs.LO
Forward and Backward Bisimulations for Chemical Reaction Networks
基于常微分方程，给出了两个具有语义的化学反应网络（CRN）物种之间的定量行为等价关系。前向CRN互模拟识别一个分区，其中每个等价类表示属于该类的物种浓度的精确总和。向后CRN互模拟涉及从相同初始条件开始时在所有时间点具有相同解的物种。这两个概念都可以只使用CRN语法信息来检查，即，通过检查反应的集合。我们提供了一个统一的算法，计算我们的互模拟在多项式时间的粗细化。此外，我们给出了算法来计算商CRNs引起的互模拟。作为一个应用程序，我们发现显着减少的一些模型的生物过程中的文献。在两种情况下，我们允许分析基准模型，否则将难以处理，由于其内存要求。
2015-07-15 cs.LO
An O(m log n) Algorithm for Stuttering Equivalence and Branching Bisimulation
我们提供了一个新的算法来确定口吃等价与时间复杂度$O(m \log n)$，其中$n$是状态的数量和$m$是一个Kripke结构的转换的数量。该算法也可用于确定$O(m(\log |\mathit{Act}|+ \log n))$时间上的分支互模拟，其中$\mathit{Act}$是标记迁移系统中的动作集。从理论上讲，我们的算法大大提高了现有的算法，所有的时间复杂度$O(m n)$在最好的。而且，它具有更好或相等的空间复杂度。实际结果证实了这些发现，表明我们的算法可以优于现有的算法的数量级，特别是当Kripke结构的大小是大的。我们的算法的重要性远远超出了口吃等价和分支互模拟。已知的$O(m n)$算法已经比大多数其他算法更有效（在空间和时间上），以确定行为等价（包括弱互模拟），因此它经常被用作一个必不可少的预处理步骤。这种新的算法使得使用口吃等价和分支互模拟更有吸引力。
2016-01-07 cs.DS cs.LO
Cost Preserving Bisimulations for Probabilistic Automata
概率自动机构成了并发概率系统的通用和优雅的模型。他们配备了一个组合理论支持抽象，使弱概率互模拟作为参考概念，总结抽象的效果。本文考虑了增加成本的概率自动机。它扩展了概率自动机中弱转换的概念，使得沿着弱转换产生的成本被捕获。这就产生了成本保持和成本约束的变化弱概率双相似性，我们建立组合属性相对于并行组合。此外，多项式时间的决策算法，提出了，可以有效地用于计算马尔可夫决策过程中的组合方式的回报约束抽象。
2015-02-16 cs.FL cs.LO
A Stochastic Game Approach to Masking Fault-Tolerance: Bisimulation and Quantification
我们引入了一个正式的概念掩蔽容错概率转移系统之间的一个变种的基础上的概率互模拟（称为掩蔽模拟）。我们还提供了相应的概率博弈特征。即使这些游戏可能是无限的，我们提出了一个象征性的方式来表示它们，这样，它可以决定在多项式时间，如果有两个概率转移系统之间的掩蔽模拟。我们使用这个掩蔽的概念来量化几乎肯定失败的系统所表现出的掩蔽容错水平，即，那些最终以概率1失败的系统几乎必然失效系统的掩蔽容错水平可以通过求解一组函数方程来计算。我们在最小化玩家以强公平方式（模仿公平环境的想法）行为的设置中产生这个度量，并将我们的研究限制在无记忆策略上，因为游戏的无限性质。我们在一个原型工具中实现了这些想法，并进行了实验评估。
2022-07-05 cs.LO
Efficient Local Computation of Differential Bisimulations via Coupling and Up-to Methods
我们引入多项式耦合，概率耦合的推广，开发一个算法的等价关系的计算，可以被解释为一个提升的概率互模拟多项式微分方程，一个无处不在的模型的动力系统在科学和工程。该算法具有多项式时间的复杂性，并补充了经典的分区细化方法，因为：（a）它实现了系统的本地探索，可能产生的等价，不一定涉及整个系统的检查微分方程;（b）它可以增强技术;（c）它允许规范的对不应该被包括在输出中。使用一个原型，这些优势被证明从系统生物学的应用程序模型简化和比较的案例研究。值得注意的是，我们报告四个数量级较小的运行时间比分区细化方法时反驳马尔可夫链之间的等价性。
2021-04-27 cs.LO
Bisimulations and Modal Logics for Higher Dimensional Automata
Norwegian University of Science and Technology（挪威科技大学）；University of Edinburgh（爱丁堡大学）；University of New South Wales（新南威尔士大学）；University of Warsaw（华沙大学）
该研究针对高维自动机，提出介于ST与hhp互模拟间的新中间等价关系，构建了刻画hhp互模拟的模态逻辑，其片段可刻画ST互模拟及中间概念。
2026-08-17 cs.LO
Probabilistic Bisimulations for PCTL Model Checking of Interval MDPs
Puggelli等人最近研究了具有凸不确定性的MDP的PCTL性质的验证。然而，模型检验算法通常遭受状态空间爆炸。在本文中，我们解决概率互模拟，以减少这样的MDP的大小，同时保持PCTL性能，它满足。我们讨论了在文献中研究的模型中的不确定性的不同解释，并导致两种不同的互模拟定义。我们给出了算法来计算这些互模拟的时间多项式的模型的大小和指数的不确定分支的同分性。最后，我们通过一个案例研究表明，在实践中的大型模型可以有小的分支，并通过我们的方法可以实现大量的状态空间减少。
2014-04-10 cs.FL cs.LO
Bisimulation Equivalence of First-Order Grammars is ACKERMANN-Complete
Sénizergues（1998，2005）证明了两个具有限制静默动作的下推自动机是否弱双相似。我们提供了第一个已知的复杂性上界这个著名的问题，在等效设置的一阶文法。这ACKERMANN上限是最佳的，我们还表明，强双相似性是连续递归的自动机的状态数是固定的。
2019-01-22 cs.FL cs.LO
A meta-probabilistic-programming language for bisimulation of probabilistic and non-well-founded type systems
Yale University（耶鲁大学）；SingularityNET（奇点网）
我们引入了一个正式的元语言的概率编程，能够表达程序和类型系统中，他们被嵌入。我们的动机是希望AGI不仅学习相关知识（程序/证明），而且学习适当的推理方式（逻辑/类型系统）。我们利用立方类型论和依赖类型元图的框架来形式化我们的方法。在这样做时，我们表明，元语言中的特定结构可以通过互模拟（意味着路径等价）与它们对应的类型系统相关。这使得我们的方法提供了一种方便的方法来派生合成指称语义的各种类型系统。特别是，我们推导出纯型系统（PTS）和概率依赖型系统（PDTS）的互模拟。我们进一步讨论了PTS的关系，非良基集理论，并证明了我们的方法的可行性与实现的互模拟证明在一个守护立方类型论类型检查。
2022-08-16 cs.AI cs.FL cs.LO
A Strong Bisimulation for a Classical Term Calculus
本文通过引入修订的 λμ-演算 ΛM 和关系 ≃，解决了 Laurent 的 ≃σ-等价在经典项演算中无法构成强互模拟的问题，并证明 ≃ 是 ΛM 归约下的强互模拟。
2024-04-17 cs.LO
History-Preserving Bisimulations on Reversible Calculus of Communicating Systems
历史互模拟和遗传互模拟（HPB和HHPB）是并发指称模型的等价关系。在进程代数中寻找它们的对应物是一个开放的问题，有一些部分的成功：在通信系统演算（CCS）中存在一个基于因果树的等价物，对应于HPB。在可逆CSS（RCCS）中，有一个对应于HHPB的互模拟，但它只考虑没有自动并发的进程。我们提出了等价的CCS与自动并发对应的HPB和HHPB，和他们所谓的“弱”的变种。等价性不仅利用了RCCS的可逆性，而且利用了RCCS的记忆机制。
2018-04-27 cs.DC cs.FL cs.LO
Bisimulation of Labelled State-to-Function Transition Systems Coalgebraically
标号状态-函数转换系统，简称FuTS，是一般半环上的状态-函数转换系统，具有丰富的高阶算子集.因此，FuTS构成了一个方便的建模工具，以处理过程语言，特别是其定量扩展。在本文中，互模拟诱导的FuTS的概念是从一个coalgebraic的角度来看。一个对应的结果是建立说明FuTS-双相似性符合行为等价的相关函子。作为一般的例子，基本的定量过程代数的主要例子的实质性片段的等价关系到特定的FuTS的双相似性。示例范围从随机过程语言PEPA到交互式马尔可夫链语言IML、（离散）定时过程语言TPC和马尔可夫自动机语言MAL。这些语言的等效性与其特定FuTS的双相似性有关。利用对应结果，得到了这些演算等价的共代数证明。语言的具体选择，除了涵盖了大量的过程交互模型和涉及数量的建模选择，使我们能够显示不同类别的FuTS，即所谓的简单FuTS，组合FuTS，嵌套FuTS，和一般FuTS。
2015-12-21 cs.LO
Computation Tree Logic with Deadlock Detection
研究了在没有下一状态模态的计算树逻辑（CTL-X）中满足相同公式的标号迁移系统的状态等价关系。这个关系是由De Nicola & Vaandrager通过将标记转移系统转化为Kripke结构而得到的，同时解除了对后者的总体性限制。他们将其描述为发散敏感分支互模拟等价。我们发现，这种等价未能成为一个交错并行组合的同余。原因是，CTL-X的非总Kripke结构的拟议应用缺乏表现力，以应付死锁属性是重要的，在并行组合的上下文中。我们提出了一个扩展的CTL-X，或替代治疗的非整体，填补这一空白。等价诱导我们的扩展的特点是分支互模拟等价与明确的分歧，这是，此外，示出的粗同余包含在分歧敏感的分支互模拟等价。
2009-12-22 cs.LO
On path-based coalgebras and weak notions of bisimulation
众所周知，余代数理论提供了行为等价的抽象定义，这与各种基于状态的系统之间的强互模拟相一致。不幸的是，在所谓的沉默行动存在的理论尚未完全发展。在本文中，我们给出了标记转移系统和完全概率系统的分支互模拟的一个共代数刻画。它示出，记录执行（直到一个概念的口吃），而不是一组后继状态，从一个状态是足够的分支互模拟在这两种情况下。
2017-05-30 cs.LO
Generalized Vietoris Bisimulations
我们引入并研究了Stone空间上余代数的互模拟[14]。我们的互模拟概念对于行为等价是合理和完整的，并且推广了Vietoris互模拟[4]。本文的主要结果是：$\mathbf{Stone}$余代数的互模拟是其基础$\mathbf{Set}$余代数的互模拟的拓扑闭包.
2014-12-15 cs.LO math.LO
A van Benthem Theorem for Quantitative Probabilistic Modal Logic
在概率转换系统中，行为度量提供了比双相似性概念更细粒度和更稳定的系统等价性度量。它们与定量概率逻辑密切相关，事实上，在实数单位区间取值的概率模态逻辑引起的距离与行为距离一致。对于概率系统，概率模态逻辑扮演着类似于Hennessy-Milner逻辑在经典标记转移系统上的角色。在定量背景下，模态逻辑在双相似性下的不变性成为公式求值的非扩展性。行为距离在本文中，我们提供了一个表征的表达能力的概率模态逻辑的基础上，这一观察：我们证明了一个概率模拟的经典范Bentham定理，它指出，模态逻辑正是一阶逻辑的互模拟不变的片段。具体来说，我们表明，定量概率模态逻辑在于密集的双模拟不变片段，在非扩展公式评估的指示意义上，定量概率一阶逻辑;更确切地说，双模拟不变的一阶公式是近似的模态公式的有界秩。有关同一结果的描述逻辑透视图，请参见arXiv：1906.00784。
2019-06-04 cs.LO
Computing Stuttering Simulations
口吃互模拟是一个著名的行为等价，它保留了CTL-X，即没有下一次操作符X的CTL。相应地，口吃模拟前序诱导了一个更粗糙的行为等价，它保留了存在片段ECTL-{X，G}，即没有下一次X和全局G算子的ECTL。虽然口吃互模拟等价可以通过著名的Groote和Vaandrager的[1990]算法计算，但据我们所知，没有计算口吃模拟前序和等价的算法。本文针对有限状态系统提出了这样一种算法。
2009-04-09 cs.LO
Splitter Orderings for Probabilistic Bisimulation
针对概率模型互模拟划分的迭代计算瓶颈，本文提出分割块排序启发式与哈希表加速技术，在常规案例研究中将运行时间平均降低一个数量级。
2023-07-17 cs.LO cs.PF cs.SE
Lax functors and coalgebraic weak bisimulation
我们推广的工作Sobocialski关系预层和他们的连接弱（双）模拟标记transition系统的一个coalgebraic设置。我们表明，在我们以前的工作中研究的饱和度的coalgebraic概念可以表示在宽松函子的语言中存在一定的adjunction类别之间的宽松函子。这一观察使我们能够推广的概念的coalgebraic弱互模拟宽松函子。我们实例化这一定义的两个例子的时间系统，并表明，它符合他们的时间抽象的行为等价。
2015-11-01 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
Scalable Minimization Algorithm for Partial Bisimulation
Eindhoven University of Technology（埃因霍温理工大学）
提出一种高效算法计算标记迁移系统的部分互模拟预序和等价，通过利用互模拟动作子集实现可扩展的最小化。
2012-07-10 cs.LO cs.SY eess.SY
Fully Abstract Normal Form Bisimulation for Call-by-Value PCF
本文为传值调用 PCF 提出首个完全抽象的范式互模拟，通过融合应用式、环境互模拟与博弈语义的 LTS 实现程序等价检查，并开发有界工具验证了文献示例与新案例。
2023-10-02 cs.LO cs.PL
Approximate reasoning for real-time probabilistic processes
我们开发了一个伪度量模拟广义半马尔可夫过程的互模拟。这个伪度量的内核对应于互模拟，因此我们已经扩展了连续时间概率过程的互模拟到比指数分布更广泛的一类分布。这种伪度量在模型中存在数值信息（如概率和时间）的情况下，对近似推理提供了有用的处理。给出了伪度量的不动点刻画。这使得可用于推理距离的共归纳推理原则。我们表明，我们的方法是不敏感的潜在特设关节的距离表明，它是内在的一个基本的均匀性。我们提供了一个逻辑表征这种一致性使用实值模态逻辑。我们表明，几个感兴趣的定量性质是连续的伪度量。因此，如果两个过程在度量上接近，那么感兴趣的可观察的定量性质确实接近。
2006-03-08 cs.LO
A Trace Based Bisimulation for the Spi Calculus
一个开放互模拟的概念制定的spi演算，一个扩展的pi演算与密码原语。在这个公式中，开放互模拟是由成对的符号迹索引的，符号迹表示环境与被检查的过程对之间的相互作用的历史。符号迹的使用允许在互模拟检查中对约束输入进行符号处理，这避免了对输入值的量化。证明了开放双相似性在等价性检验方面是合理的，并进一步证明了开放双相似性是过程上的等价关系和有限过程上的同余关系。据我们所知，这是第一个制定的开放互模拟的spi演算的全等结果得到证明。
2009-01-15 cs.CR cs.LO
Logic-Induced Bisimulations
对于由逻辑连接给出的共代数模态逻辑，我们定义了一个新的逻辑诱导的互模拟概念（称为$ρ$ -互模拟），并研究了它的性质。我们表明，它是结构的意义上说，它是只在定义方面的余代数结构和一步模态语义，而且，可以通过一种形式的关系提升的特点。此外，我们比较$ρ$ -互模拟几个著名的等价概念，我们证明了两个模型之间的互模拟的集合往往形成一个完整的晶格。主要的技术结果是一个Hennessy-Milner型定理，它指出，在某些条件下，逻辑等价意味着$ρ$ -双相似性。特别地，后者不依赖于函子\emph{not}（余代数的类型）和$\mathsf{L}$（给出逻辑）之间的对偶性，也不依赖于逻辑连接$ρ$的属性。
2020-08-21 cs.LO math.LO
Resource Bisimilarity in Petri Nets is Decidable
本文针对 Petri 网中的资源互模拟关系，提出判定算法，证明其可判定性，并给出相似但不互模拟的实例，区别于不可判定的资源相似性。
2022-10-03 cs.LO
Improving Probabilistic Bisimulation for MDPs Using Machine Learning
本文提出利用PRISM程序构建小模型并训练分类器，用机器学习近似概率互模拟划分，将其作为标准互模拟方法的初始划分，从而显著降低MDP互模拟最小化的运行时间。
2023-07-30 cs.LG cs.LO cs.PF
Qualitative Logics and Equivalences for Probabilistic Systems
我们调查的逻辑和等价关系，捕捉定性行为的马尔可夫决策过程（MDP）。我们提出了定性随机CTL（QRCTL）：这种逻辑公式可以表达这样一个事实，即某些时间属性持有所有路径，或概率为0或1，但它们不区分中间概率值。我们提出了一个符号的，多项式时间模型检测算法的QRCTL MDP。逻辑QRCTL在MDP的状态上导出了一个等价关系，我们称之为定性等价：非正式地说，如果两个状态下概率为0或1的公式集相同，则两个状态是定性等价的。我们表明，对于有限的交替MDP，其中不确定性和概率的选择发生在不同的状态，定性等价与交替互模拟相吻合，因此可以通过有效的分区细化算法计算。另一方面，在非交替MDP中，等价关系不能通过划分细化算法来计算，而是需要非局部计算。最后，我们考虑QRCTL*，它以与CTL* 扩展CTL相同的方式用嵌套的时态运算符扩展QRCTL。我们表明，QRCTL和QRCTL* 诱导交替MDP相同的定性等价，而在非交替MDP，从QRCTL* 产生的等价可以严格更精细。我们还提供了一个完整的定性等价，互模拟，交替互模拟之间的关系的表征，根据是否MDP是有限的，以及他们的过渡关系是否是有限分支。
2009-05-04 cs.LO
How Reversibility Can Solve Traditional Questions: The Example of Hereditary History-Preserving Bisimulation
可逆计算开辟了克服硬件当前物理限制的可能性。它还提供了理论上的见解，因为它丰富了多种计算范式和模型，有时回顾性地启发它们。例如，并发可逆计算为通信系统微积分提供了有趣的扩展，但仍然缺乏自然和相关的互模拟来研究过程等价性。我们的论文制定了一个等价利用可逆性的两个方面：向后移动和记忆机制。这种互模拟捕获了并发性的指称模型（历史和遗传的历史保留互模拟，（H）HPB）的经典等价关系，到目前为止，进程代数只部分表征了这些模型。这一结果提供了一个洞察可逆性的表现力，因为向后移动和记忆机制，提供“向后确定性”-需要捕捉HHPB。
2020-05-14 cs.DC cs.FL cs.LO
Strong Bisimulation for Control Operators
本文的目的是确定程序的控制运营商的减少语义是在确切的对应关系。这是通过引入一个关系$\simeq$来实现的，该关系定义在Parigot的$λμ$的修正表示上-我们称之为$ΛM$的演算。我们的结果建立在两个基本成分上：（1）通过$ΛM$的显式项算子将$λμ$ -归约分解为乘法和指数步骤，以及（2）将$ΛM$ -项转换为Laurent的极化证明网（PPN），使得PPN中的割消模拟我们的演算。我们提出的关系$\simeq$的PPN结构等价的特点。最值得注意的是，$\simeq$被证明是一个强大的互模拟相对于减少$ΛM$，即两个$\simeq$ -等价的条款有完全相同的减少语义，一个结果，这失败的Regnier的$σ$ -等价的$λ$ -演算以及劳伦特的$σ$ -等价的$λμ$。
2019-10-16 cs.LO cs.PL
