并发进程的弱马尔可夫互模拟同余和精确CTMC级集结

基于可聚类的强随机互模拟与弱随机互模拟及其同余性质的分类法

A Lumpability-Driven Taxonomy of Strong and Weak Stochastic Bisimilarities with Their Congruence Properties

本文统一了PEPA中基于CTMC可聚类性的六种随机互模拟，建立包含关系分类法，并分析其同余性质。

用于凸和抽象概率互模拟的SOS规则格式

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）“概率抽象互模拟”，其与互模拟一样，保留分布的结构，但相反，其忽略概率值。此外，我们比较这些互模拟等价，并为他们每个人提供了一个逻辑表征。

基于迹的Spi演算互模拟

A Trace Based Bisimulation for the Spi Calculus

一个开放互模拟的概念制定的spi演算，一个扩展的pi演算与密码原语。在这个公式中，开放互模拟是由成对的符号迹索引的，符号迹表示环境与被检查的过程对之间的相互作用的历史。符号迹的使用允许在互模拟检查中对约束输入进行符号处理，这避免了对输入值的量化。证明了开放双相似性在等价性检验方面是合理的，并进一步证明了开放双相似性是过程上的等价关系和有限过程上的同余关系。据我们所知，这是第一个制定的开放互模拟的spi演算的全等结果得到证明。

一种用于概率过程的新分支双模拟

A New Branching Bisimulation for Probabilistic Processes

该研究为概率过程引入新分支双模拟，此双模拟诱导出更精细等价关系，其有根版本对含递归等构造的概率过程语言是同余关系，是一种新的等价关系定义。

Enabling Preserving Bisimulation Equivalence

Most fairness assumptions used for verifying liveness properties are criticised for being too strong or unrealistic. On the other hand, justness, arguably the minimal fairness assumption required for the verification of liveness properties, is not preserved by classical semantic equivalences, such as strong bisimilarity. To overcome this deficiency, we introduce a finer alternative to strong bisimilarity, called enabling preserving bisimilarity. We prove that this equivalence is justness-preserving and a congruence for all standard operators, including parallel composition.

Abstract Congruence Criteria for Weak Bisimilarity

We introduce three general compositionality criteria over operational semantics and prove that, when all three are satisfied together, they guarantee weak bisimulation being a congruence. Our work is founded upon Turi and Plotkin's mathematical operational semantics and the coalgebraic approach to weak bisimulation by Brengos. We demonstrate each criterion with various examples of success and failure and establish a formal connection with the simply WB cool rule format of Bloom and van Glabbeek. In addition, we show that the three criteria induce lax models in the sense of Bonchi et al.

组态结构上的可逆倒钩同余

Reversible Barbed Congruence on Configuration Structures

进程代数的一个标准上下文等价是强倒钩同余。配置结构是进程的指称语义，其中可以定义更具区分性的等价物，即区分由带刺同余等同的术语的指称。遗传历史保持互模拟（HHPB）就是这样一种关系。我们定义了一个强的来回倒钩同余使用可逆的过程代数，并表明，由来回同余引起的关系是等价的HHPB，HHPB提供了一个上下文表征。

Petri 网中的资源互模拟是可判定的

Resource Bisimilarity in Petri Nets is Decidable

本文针对 Petri 网中的资源互模拟关系，提出判定算法，证明其可判定性，并给出相似但不互模拟的实例，区别于不可判定的资源相似性。

具有死锁检测的计算树逻辑

Computation Tree Logic with Deadlock Detection

研究了在没有下一状态模态的计算树逻辑（CTL-X）中满足相同公式的标号迁移系统的状态等价关系。这个关系是由De Nicola & Vaandrager通过将标记转移系统转化为Kripke结构而得到的，同时解除了对后者的总体性限制。他们将其描述为发散敏感分支互模拟等价。我们发现，这种等价未能成为一个交错并行组合的同余。原因是，CTL-X的非总Kripke结构的拟议应用缺乏表现力，以应付死锁属性是重要的，在并行组合的上下文中。我们提出了一个扩展的CTL-X，或替代治疗的非整体，填补这一空白。等价诱导我们的扩展的特点是分支互模拟等价与明确的分歧，这是，此外，示出的粗同余包含在分歧敏感的分支互模拟等价。

区间马尔可夫决策过程的合成推理

Compositional Reasoning for Interval Markov Decision Processes

Puggelli等人最近研究了具有凸不确定性的Markov决策过程的模型检验概率CTL性质，这类模型检验算法通常存在状态空间爆炸问题.在本文中，我们解决概率互模拟，以减少这样的MDP的大小，同时保持概率CTL属性，它满足。特别是，我们讨论的关键成分，建立在运行时组成间隔MDP组件的并行组合操作。更确切地说，我们研究如何并行组合操作的区间MDP可以定义，以便达到一个同余闭包。其结果是，我们表明，概率互模拟区间MDPs是一致的两个方面的并行性，即同步产品和交织。

全局控制的会话语义

Globally Governed Session Semantics

本文提出了一种基于多方会话类型的互模拟理论，其中编排规范管理会话类型进程及其观察者的行为。互模拟的定义与观察者与所观察到的进程合作，以形成完整的全局会话场景，并可用于证明全局协调线程和进程的优化的正确性。诱导互模拟比标准会话互模拟严格地更细粒度。只有当存在两个以上的交错多方会话时，受控制的互模拟和标准互模拟之间的差异才会出现。这个独特的功能使得能够在大规模分布式系统中推理真实场景，其中多个编排会话需要交错。通过关于受支配的基于约简的同余的可靠性和完备性，证明了受支配的双相似性的组合性。最后，在一个大规模网络基础架构的实际应用中，通过一个多会话控制下的线程转换演示了该方法的使用。

进程代数CCS在HOL4中的进一步形式化

Further Formalization of the Process Algebra CCS in HOL4

在这个项目中，我们已经扩展了以前的工作在HOL4的进程代数CCS的形式化。我们增加了对弱互模拟等价和观测同余（有根弱等价）的完全支持，以及相关的定义、定理和代数定律。一些深引理也在这个项目中得到了形式化的证明，包括邓引理、Hennessy引理和几种版本的“弱等价中包含的Coarse同余”。对于最后一个定理，我们已经证明了基于序数的完整版本（没有任何假设）。

Divide and Congruence III: From Decomposition of Modal Formulas to Preservation of Stability and Divergence

In two earlier papers we derived congruence formats with regard to transition system specifications for weak semantics on the basis of a decomposition method for modal formulas. The idea is that a congruence format for a semantics must ensure that the formulas in the modal characterisation of this semantics are always decomposed into formulas that are again in this modal characterisation. The stability and divergence requirements that are imposed on many of the known weak semantics have so far been outside the realm of this method. Stability refers to the absence of a $τ$-transition. We show, …

配置结构中的上下文等价性和可逆性

Contextual equivalences in configuration structures and reversibility

上下文等价将在任何上下文中具有相同可观察行为的术语等同起来。CCS的一个标准上下文等价是强倒钩同余。配置结构是一种进程的指称语义，其中定义了更具区分性的等价，即区分由带刺的同余所等同的项的指称。遗传历史保持互模拟（HHPB）就是这样一种关系。我们定义了一个强的来回倒钩同余RCCS，CCS的可逆变种。我们表明，由配置结构上的前后一致引起的关系是等价的HHPB，从而提供了一个上下文表征HHPB。

公理化平坦迭代

Axiomatizing Flat Iteration

平坦迭代是Kleene星运算P*Q的原始二进制版本的变体，通过将第一个参数限制为原子动作的总和而获得。它推广了前缀迭代，其中第一个参数是单个操作。给出了基本CCS上具有平坦迭代的互模拟同余的5个概念，即强同余、分支同余、η-同余、延迟同余和弱同余的完全有限方程公理化.这样的公理化对于前缀迭代是已知的，而对于一般迭代则不存在。与前缀迭代相比，使用平坦迭代有两个主要优点：1.现有的公理化方法推广到了完全CCS，而前缀迭代方法不允许异步并行复合算子的消去定理。2.平坦迭代的更大表达性允许更短的完整性证明。在前缀迭代的情况下，得到eta-、时滞和弱同余的完备性定理的最方便的方法是将分支同余的完备性定理化为分支同余的完备性定理。在弱同余的情况下，这原来是简单得多，比唯一的直接证明发现。在设置平坦的迭代另一方面，完整性定理延迟和弱（但不是eta-）同余可以同样很好地得到减少到一个强同余，而不使用分支同余作为中间步骤。此外，前缀迭代的完备性结果可以从平坦迭代的完备性结果中得到，从而得到了前缀迭代情形下时滞和弱同余完备性的第二种间接证明方法.

马尔可夫自动机的期望延迟求和弱双相似性

Expected-Delay-Summing Weak Bisimilarity for Markov Automata

一个新的弱互模拟语义定义的马尔可夫自动机，除了抽象的内部行动，总结了连续的指数分布的延迟可能交织在一起的内部行动的期望值。由此产生的等价证明是一个同余相对于并行组成的马尔可夫自动机。此外，它原来是可比的弱双相似定时标记的过渡系统，从而构成了一个步骤，调和的语义随机时间和确定性时间。

关于反应式系统中的倒钩和标号

On Barbs and Labels in Reactive Systems

反应式系统（RS）表示一个元框架，旨在为那些由归约规则提供操作语义的计算形式主义导出行为一致性。RS被证明是一种灵活的规范设备，但到目前为止，大多数处理其行为语义的努力都集中在同素推出（IPO）和饱和（也称为动态）互模拟上。在本文中，我们介绍了一种新的，中间的行为等价：L-双相似性，这是能够重铸其IPO和饱和的同行。的等价性是参数的一组L的RS标签，它表明，在温和的条件下L，它确实是一个同余。此外，L-双相似性还可以改写RS的倒钩语义的概念，这是由同一作者在以前的论文中提出的。为了提供一个合适的测试床，我们实例化我们的建议，解决（异步）CCS的语义和演算的移动环境。

Rocq中域理论与交互树的结合

Domain Theory Meets Interaction Trees in Rocq

本研究在Rocq中提出不依赖内置共归纳的域理论交互树形式化方法，定义归纳式程序等价关系以简化非终止程序推理，证明其正确性并通过叙拉古序列程序示例验证框架。

高阶概率泛函程序的共归纳等价性（长版）

On Coinductive Equivalences for Higher-Order Probabilistic Functional Programs (Long Version)

我们研究互模拟和上下文等价的概率$λ$演算。本文的贡献有三个方面。首先，我们展示了一种证明概率应用双相似同余的技术。虽然该技术遵循豪的方法，但一些技术细节是完全不同的，依赖于实数集的非平凡“解开”属性。其次，我们表明，虽然双相似性是在一般情况下严格比上下文等价，这两个关系之间的重合达到纯$λ$ -条款。由此产生的等式是由Levy-Longo树诱导的等式，通常被认为是在懒惰制度下纯$λ$ -项上的最好的扩展等价。最后，我们推导出一个共归纳特征的上下文等价的整个概率语言，通过一个扩展，其中条款类似于分布可能会出现在redex的位置。扩展的另一个动机是它的操作语义允许我们实验不同的一致性技术，即逻辑双相似性。

量子过程的观测等价性

Observational Equivalence Using Schedulers for Quantum Processes

在量子过程代数的研究中，研究人员引入了不同的量子过程之间的等价概念，如互模拟或倒刺同余。然而，有一些直观上等价的量子过程，这些概念并不认为是等价的。本文在qCCS中引入了观测等价的概念。由于量子过程既有概率跃迁又有非确定跃迁，因此我们引入了求解非确定选择并获得量子过程概率分布的求解器。从定义上讲，观测者的限制改变了观测等价性。给出了观测等价的定义，并讨论了观测等价与观测等价的关系。