Proving Continuity of Coinductive Global Bisimulation Distances: A Never Ending Story
我们已经开发了一个概念的全球互模拟距离的进程之间的某种程度上超越了互模拟距离的概念已经存在于文献中，主要是基于互模拟游戏。我们的建议是基于转换的成本：我们需要修改一个比较的过程来获得另一个。我们最初的定义只覆盖有限的过程，但共归纳的方法允许我们将其扩展到覆盖无限但有限的树。在展示了我们距离的许多有趣性质之后，我们打算证明关于投影的连续性，但不幸的是，这个问题仍然悬而未决。尽管如此，我们已经得到了一些部分的结果，在本文中提出。
2015-12-22 cs.LO
Distribution-based bisimulation for labelled Markov processes
在本文中，我们提出了一个（子）分布为基础的互模拟标记马尔可夫过程，并将其与早期的定义状态和事件的互模拟，这两个比较状态。与那些基于状态的互模拟相比，我们的分布互模拟更弱，但更接近于线性性质。我们构建了一个逻辑和一个度量来描述我们的分布互模拟，并讨论了线性，连续性和组成特性。
2017-06-30 cs.FL cs.LO
On Context Bisimulation for Parameterized Higher-order Processes
本文研究高阶过程在参数化（即抽象）条件下的上下文互模拟。我们表明，高阶过程的扩展与过程参数化保留了上下文互模拟的特征，由一个更简单的形式的互模拟称为正常的互模拟（即。他们是一致的），其中全称量词被淘汰，而它是不一样的名称参数化。这些结果进一步阐明了高阶过程的互模拟理论，也揭示了两种参数化的本质区别。
2013-10-17 cs.GT cs.LO
Open Bisimulation for Quantum Processes
量子过程描述了可能涉及量子信息的并发通信系统。我们提出了一个开放互模拟量子过程的概念，并表明，它提供了一个健全的和完整的证明方法，量子过程之间的自然扩展行为等价。我们还给出了一个模态特征的开放互模拟，通过扩展的Hennessy-Milner逻辑的量子设置。
2012-01-02 cs.LO quant-ph
Unprovability of the Logical Characterization of Bisimulation
我们快速审查标记马尔可夫过程（LMP），并提供了一个反例表明，在一般的可测空间，事件双相似性和状态双相似性不同的LMP。这表明，Desharnais [*]中的逻辑在非解析可测空间中不刻画状态互模拟。此外，我们表明，根据目前的数学基础，这样的逻辑特征是不可证明的空间，是一个协分析集的投影。在这个结构的基础上，证明了一般可测空间上的平稳马尔可夫过程不具有半拉回。[1] J. Desharnais，Labelled Markov Processes。计算机科学学院。蒙特利尔麦吉尔大学（1999年）
2010-12-10 cs.LO
Finitary Truly Concurrent Bisimulations
为基于预互模拟预序的过程语言开发完全抽象指称模型，解决无限观察区分问题，定义真正并发预互模拟及其有限形式。
2026-06-09 cs.LO
Logical Characterization of Bisimulation Metrics
互模拟度量为研究不确定性概率过程的行为提供了一种鲁棒而精确的方法。在本文中，我们提出了一个简单的概率变化的Hennessy-Milner逻辑的基础上的互模拟度量的逻辑表征。我们的方法是基于新的概念，模仿公式和公式之间的距离。前者是一个弱版本的著名的特征公式，并允许我们也（准备）概率模拟和概率双相似性的特点。后者是一个1-有界伪度量的公式，反映了Hausdorff和Kantorovich提升定义的双相似伪度量。我们证明了两个过程之间的距离等于它们自己的模仿公式之间的距离。
2016-10-26 cs.LO
Bisimulation for quantum processes
在本文中，我们引入了一个新的概念，量子过程的概率互模拟，并证明它是全等的各种进程代数组合子，包括并行组合，即使经典和量子通信。我们还建立了一些基本的代数规律，这种互模拟。特别地，我们证明了量子过程的递归方程的解的唯一性，这为验证复杂的量子协议提供了一个强有力的证明技术。
2013-11-14 cs.LO quant-ph
Witnesses and Counterexamples for Timed Bisimulation
TU Darmstadt（达姆施塔特工业大学）；University of Siegen（锡根大学）
针对时间自动机互模拟验证，提出基于虚拟时钟扩展区域图的方法，既能有效检查时间互模拟等价，又能生成有效见证或反例解释行为差异。
2026-06-16 cs.FL cs.LO
Approximate Bisimulation and Discretization of Hybrid CSP
混合通信顺序过程（Hybrid Communicating Sequential Processes，HCSP）是一种功能强大的混合系统形式化建模语言，它是CSP的扩展，通过引入微分方程来建模连续演化，引入中断来建模连续动态与离散动态之间的相互作用。在本文中，我们调查的语义基础HCSP从操作的角度来看，提出了近似互模拟的概念，它提供了一个适当的标准来表征HCSP过程之间的等价性与连续和离散的行为。给出了一个判定两个HCSP过程是否近似双相似的算法。此外，在此基础上，我们提出了一种离散化HCSP的方法，即，给定一个HCSP过程A，我们构造另一个HCSP过程B，它不包含任何连续动力学，使得A和B在给定精度下近似双相似。这提供了一个严格的方法来转换一个验证的控制模型到一个正确的程序模型，这填补了在嵌入式系统的设计空白。
2016-09-08 cs.LO
Bisimulation for Feller-Dynkin Processes
针对演化呈时间流的连续时间随机过程，提出两种等价的互模拟定义，证明其限制到离散时间时涵盖标准离散时间概念，且并非离散概念的直接推广。
2019-04-01 cs.FL cs.LO math.PR
Globally Governed Session Semantics
本文提出了一种基于多方会话类型的互模拟理论，其中编排规范管理会话类型进程及其观察者的行为。互模拟的定义与观察者与所观察到的进程合作，以形成完整的全局会话场景，并可用于证明全局协调线程和进程的优化的正确性。诱导互模拟比标准会话互模拟严格地更细粒度。只有当存在两个以上的交错多方会话时，受控制的互模拟和标准互模拟之间的差异才会出现。这个独特的功能使得能够在大规模分布式系统中推理真实场景，其中多个编排会话需要交错。通过关于受支配的基于约简的同余的可靠性和完备性，证明了受支配的双相似性的组合性。最后，在一个大规模网络基础架构的实际应用中，通过一个多会话控制下的线程转换演示了该方法的使用。
2015-03-01 cs.LO
On the Complexity of Robust Markov Decision Processes and Bisimulation Metrics
University of Antwerp（安特卫普大学）
本文研究了鲁棒马尔可夫决策过程在多面体不确定性集下的复杂性，证明了(s,a)-矩形RMDP的鲁棒策略评估在P中，阈值问题在NP中，同时通过将奇偶游戏和马尔可夫过程状态间的仿射度量归约到RMDP阈值问题，建立了下界。
2026-06-25 cs.LO
Approximate reasoning for real-time probabilistic processes
我们开发了一个伪度量模拟广义半马尔可夫过程的互模拟。这个伪度量的内核对应于互模拟，因此我们已经扩展了连续时间概率过程的互模拟到比指数分布更广泛的一类分布。这种伪度量在模型中存在数值信息（如概率和时间）的情况下，对近似推理提供了有用的处理。给出了伪度量的不动点刻画。这使得可用于推理距离的共归纳推理原则。我们表明，我们的方法是不敏感的潜在特设关节的距离表明，它是内在的一个基本的均匀性。我们提供了一个逻辑表征这种一致性使用实值模态逻辑。我们表明，几个感兴趣的定量性质是连续的伪度量。因此，如果两个过程在度量上接近，那么感兴趣的可观察的定量性质确实接近。
2006-03-08 cs.LO
On the Axiomatisation of Branching Bisimulation Congruence over CCS
在本文中，我们调查的方程理论（限制，重新标记，和递归自由片段）CCS模扎根分支双相似性，这是一个经典的，基于bisimulation的概念等价的抽象过程中的行为从内部计算步骤。首先，我们证明了CCS不是基于模所考虑的同余。作为一个关键步骤的独立利益的证明，否定的结果，我们证明了每个CCS进程有一个独特的并行分解成不可分解的过程模分支双相似性。作为第二个主要贡献，我们表明，当一组行动是有限的，根分支双相似性有一个有限的方程基础上CCS丰富的左合并和通信合并运营商从ACP。
2022-06-28 cs.LO
Parallel Pushdown Automata and Commutative Context-Free Grammars in Bisimulation Semantics (Extended Abstract)
本文研究了在互模拟语义下，将经典下推自动机与上下文无关文法等价定理扩展至并行下推自动机与带并行性进程代数的情况。
2023-09-13 cs.LO
Generating Witness of Non-Bisimilarity for the pi-Calculus
在逻辑编程范式中，很难开发出一个优雅的解决方案来生成证明两个π演算过程之间的开放双相似性失败的区分公式;这是出乎意料的，因为π演算和开放互模拟的语义已经在高阶逻辑编程系统中被优雅地指定。我们使用Haskell的解决方案将公式生成定义为从所有不确定互模拟步骤的森林到一对区分公式的树变换。由于Haskell中的惰性，只生成树转换函数所需的必要路径。我们的工作表明，Haskell和它的库提供了一个有吸引力的平台，象征性地分析等价性标记的过渡系统在环境敏感的设置。
2017-05-31 cs.LO
Sound Bisimulations for Higher-Order Distributed Process Calculus
虽然分布式系统的进程转移已经变得普遍，推理他们的行为的方法是欠发达。在本文中，我们提出了一个互模拟技术证明行为等价的\emph{higher-order $π$-calculus with passivation}（和限制）中建模的系统。以前的研究，这种演算仅限于上下文互模拟和正常的互模拟，这是不切实际的或不健全的。相比之下，我们提供了一个健全的和有用的定义\emph{environmental bisimulations}，与几个非平凡的例子。从技术上讲，我们的互模拟中的一个中心点是并行组合的子句，它必须考虑在执行过程中产生的进程的钝化。
2011-05-06 cs.DC cs.LO cs.PL
From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques
我们提出了一个有界等价性验证技术的高阶程序与局部状态。该技术结合了完全抽象的符号环境互模拟类似的符号游戏语义，新的技术，轻量级的状态不变的注释。这产生了没有假阳性或假阴性的等效性验证技术。该技术是有界完备的，因为所有的不等式都是自动检测到足够大的界限。此外，几个硬等价证明自动或后被注释与状态不变量。我们在一个名为Hobbit的工具原型中实现了该技术，并使用一组广泛的新的和现有的示例对其进行基准测试。霍比特人可以证明许多经典的等价关系，包括所有迈耶和西伯的例子。
2021-10-22 cs.LO cs.PL
Compositional Reasoning for Interval Markov Decision Processes
Puggelli等人最近研究了具有凸不确定性的Markov决策过程的模型检验概率CTL性质，这类模型检验算法通常存在状态空间爆炸问题.在本文中，我们解决概率互模拟，以减少这样的MDP的大小，同时保持概率CTL属性，它满足。特别是，我们讨论的关键成分，建立在运行时组成间隔MDP组件的并行组合操作。更确切地说，我们研究如何并行组合操作的区间MDP可以定义，以便达到一个同余闭包。其结果是，我们表明，概率互模拟区间MDPs是一致的两个方面的并行性，即同步产品和交织。
2016-07-28 cs.LO
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
Bisimulation as path type for guarded recursive types
在类型论中，共归纳类型用于表示进程，因此对于基于类型论的证明助手（如Coq和Agda）中的非终止反应式程序的形式化验证至关重要。目前，关于共归纳类型的编程和推理很困难，原因有两个：需要递归定义才能高效，以及内置标识类型和重要的双相似性概念缺乏重合。中野意义上的保护递归最近被认为是处理生产力问题的一种可能方法，允许将其编码在类型中。事实上，共归纳类型可以使用保护递归和时钟上的通用量化的组合来编码。本文研究了Ticked Cubical类型论中保护递归类型的双相似性概念，Ticked Cubical类型论是Cubical类型论的一个推广。我们证明了，对于任何函子，一个抽象的，范畴论的概念，双相似的最终守护余代数是等价的（在同伦类型论的意义上），以道路平等（原始概念的平等在立方类型论）。作为一个工作的例子，我们研究了一个守卫的概念标记的过渡系统，并表明，作为一个特殊的情况下的一般定理，路径平等符合适应通常的概念互模拟过程。特别是，这意味着保护递归可以用来给简单的等式推理证明的双相似性。这项工作应该被看作是使用上述编码获得双相似性作为共归纳类型的路径相等的一步。
2018-10-31 cs.LO
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
Two behavioural pseudometrics for continuous-time Markov processes
McGill University（麦吉尔大学）；Heriot-Watt University（赫瑞-瓦特大学）
本文提出连续时间马尔可夫过程的第二种行为伪度量，基于轨迹，并与前一种伪度量进行比较。
2026-10-30 cs.LO
Core Higher-Order Session Processes: Tractable Equivalences and Relative Expressiveness
这项工作提出了易于处理的双向模拟高阶π演算会话原语（HOPI），并提供了一个完整的研究其最重要的子演算的表达能力。首先，我们开发了三种类型的互模拟，这是符合上下文对等。这些特征表明，仅观察高阶值的特定有限集合（其存在于会话类型中）作为输入就足以推理HOp过程。接下来，我们确定HO，一个最小的，二阶的HOPI子演算，其中高阶的应用程序/抽象，名称传递和递归是缺席的。我们表明，HO可以编码HOPI扩展高阶应用程序和抽象，一阶会话π演算可以编码HOPI。这两种编码都是完全抽象的。我们还证明了会话π演算与共享名称的传递不能被编码到HOPI没有共享名称。我们表明，HOPI，HO和PI是同样的表达; HO的表达能力，使有效的推理类型等价的高阶过程。
2015-02-10 cs.LO
Concurrent bisimulation algorithm
并发系统的粗互模拟发现问题在并发系统的形式化分析中起着重要的作用。例如，解决这个问题可以比较不同过程的行为或验证规范。因此，本文提出了一种有效的并发互模拟算法。它是基于顺序Paige和Tarjan算法和状态签名的概念。最初的解决方案遵循Hopcroft的原则“处理较小的一半”。所提出的算法使用其广义版本“处理所有，但最大的一个”更适合并发和并行应用程序。所实现的运行时间与最知名的顺序和并发解决方案相当。在工作的最后，进行了测试的结果。文中还讨论了最优算法运行时间的下界问题。
2014-01-10 cs.DC cs.LO
Symbolic Reachability Analysis of Higher-Order Context-Free Processes
我们考虑高阶上下文无关过程的符号可达性分析问题。这些模型是上下文无关过程（也称为BPA过程）的一般化，其中每个过程操纵一个数据结构，该数据结构可以被视为堆栈的嵌套堆栈。我们的主要结果是，对于任何高阶上下文无关的过程，一个给定的正则配置集的所有前辈的集合是正则的，有效地构造。这个结果推广了类似的结果，这是已知的1级上下文无关的过程。我们表明，这一结果也持有的情况下，向后可达性分析下，经常约束的配置。作为推论，我们得到了具有规则原子谓词的时态逻辑E（U，X）的符号模型检验算法，即，CTL片段仅限于EU和EX模式。
2007-05-28 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
A behavioural pseudometric for continuous-time Markov processes
本文推广双模拟度量概念，通过泛函不动点与实值逻辑两种等价方法，为连续时间马尔可夫过程（如布朗运动或含跳跃过程）定义行为伪度量。
2025-01-22 cs.LO
Nash Equilibrium and Bisimulation Invariance
本文发现标准策略模型下互模拟不保持纳什均衡存在性，提出三种保持该性质的策略模型，为策略推理逻辑提供新语义基础并研究受限场景。
2019-09-19 cs.LO
A Coalgebraic Model of Quantum Bisimulation
本文提出基于效应代数和分级单子的余代数模型，以定义量子并发系统的行为等价性，并推荐核互模拟以刻画对所有输入态概率行为一致的量子系统。
2025-09-25 cs.ET cs.LO
On Decidability of the Bisimilarity on Higher-order Processes with Parameterization
具有参数化的高阶过程能够抽象和应用（从微积分迁移而来），因此在计算上更具表现力。对于最小高阶并发性，众所周知，强双相似性（即，强互模拟相等）在没有参数化的情况下是可判定的。相比之下，对于参数化高阶过程，强双相似性是否仍然是可判定的仍然不清楚。在本文中，我们关注这个问题。基本上有两种参数化：一种是关于名称，另一种是关于进程。我们表明，强双相似性确实是可判定的高阶过程配备了这两种参数化。然后，我们展示了如何适应的决策方法来建立一个公理系统的强双相似性。在这些结果的基础上，我们提供了一个算法的双相似性检查。
2021-08-24 cs.LO
Static Analysis of Communicating Processes using Symbolic Transducers
我们提出了一个通用模型，允许静态分析的基础上抽象的解释系统的通信过程。我们的技术受到常规模型检验的启发，将程序状态集表示为格自动机，将程序语义表示为符号转换器。该模型可以表示进程和通信的动态创建/销毁。使用抽象的解释框架，我们能够提供一个健全的过度近似的系统的可达集，从而使我们能够证明安全属性。我们在一个原型中实现了这种方法，该原型针对C程序的MPI库。
2016-11-27 cs.FL cs.LO cs.SE
Observational Equivalence Using Schedulers for Quantum Processes
在量子过程代数的研究中，研究人员引入了不同的量子过程之间的等价概念，如互模拟或倒刺同余。然而，有一些直观上等价的量子过程，这些概念并不认为是等价的。本文在qCCS中引入了观测等价的概念。由于量子过程既有概率跃迁又有非确定跃迁，因此我们引入了求解非确定选择并获得量子过程概率分布的求解器。从定义上讲，观测者的限制改变了观测等价性。给出了观测等价的定义，并讨论了观测等价与观测等价的关系。
2014-12-30 cs.LO quant-ph
