在CCS上Split-2双相似性具有有限公理化，<br>轩尼诗&#39;的合并

Are Two Binary Operators Necessary to Obtain a Finite Axiomatisation of Parallel Composition?

Bergstra and Klop have shown that bisimilarity has a finite equational axiomatisation over ACP/CCS extended with the binary left and communication merge operators. Moller proved that auxiliary operators are necessary to obtain a finite axiomatisation of bisimilarity over CCS, and Aceto et al. showed that this remains true when Hennessy's merge is added to that language. These results raise the question of whether there is one auxiliary binary operator whose addition to CCS leads to a finite axiomatisation of bisimilarity. We contribute to answering this question in the simplified setting of th…

量子互模拟在物理可容许调度器下是一个同余关系

Quantum Bisimilarity is a Congruence under Physically Admissible Schedulers

本文通过引入物理可容许调度器丰富了CCS的线性量子扩展，解决了量子并发系统中不受约束的非确定性问题，推导出满足并行复合同余和量子有限区分能力的良态互模拟关系。

真正的并发逻辑

A Logic for True Concurrency

我们提出了一个逻辑的真正的并发性，其公式谓词的事件在计算和因果关系的依赖关系。诱导的逻辑等价是遗传的历史保持双相似性，和片段的逻辑可以被识别对应于其他真正的并发行为等价在文献中：步骤，pomset和历史保持双相似性。标准的Hennessy-Milner逻辑，因此（交织）双相似性，也被恢复为一个片段。我们还提出了一个扩展的逻辑与不动点算子，从而允许描述因果和并发性质的无限计算。我们相信，这项工作有助于合理介绍真正的并发频谱和更深入地了解所涉及的行为等价物之间的关系。

量子过程的符号互模拟

Symbolic bisimulation for quantum processes

利用文献中提出的互模拟概念，为了检验两个量子过程是否互相似，我们必须用任意量子态实例化它们的自由量子变量，并验证结果组态的互相似性。这使得从算法的角度来看，检查双相似性是不可行的，因为量子态构成了一个连续统。在本文中，我们直接在量子操作层次上引入了一种量子过程的符号操作语义，它允许我们描述量子过程之间的互模拟，而无需求助于量子态。我们表明，这里定义的符号互模拟是等价的开放互模拟量子过程在以前的工作中，当考虑强互模拟。提出了一种符号基双相似性检验算法。基于Hennessy-Milner逻辑对量子过程的扩展，我们给出了量子双相似性的模态逻辑刻画。

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

Further Formalization of the Process Algebra CCS in HOL4

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

Bisimulation and bisimilarity for fuzzy description logics under the Gödel semantics

Description logics (DLs) are a suitable formalism for representing knowledge about domains in which objects are described not only by attributes but also by binary relations between objects. Fuzzy extensions of DLs can be used for such domains when data and knowledge about them are vague and imprecise. One of the possible ways to specify classes of objects in such domains is to use concepts in fuzzy DLs. As DLs are variants of modal logics, indiscernibility in DLs is characterized by bisimilarity. The bisimilarity relation of an interpretation is the largest auto-bisimulation of that interpret…

邻域结构：双相似性与基本模型理论

Neighbourhood Structures: Bisimilarity and Basic Model Theory

邻域结构是用于推理非正规模态逻辑的标准语义工具。所有邻域模型的逻辑称为经典模态逻辑。在余代数术语中，邻域框架是与自身合成的逆变幂集函子的余代数，记为2^2。我们使用这个coalgebraic模型来推导邻域结构之间的等价概念。2^2-双相似性和行为等价是众所周知的共代数概念，它们是不同的，因为2^2不保持弱回调。我们引入第三个，中间的概念，其见证关系，我们称之为预同余（基于推出）。我们给出了2^2-互模拟和预同余的来回式特征，我们证明了在单个余代数上，预同余捕获行为等价，并且在邻域结构之间，预同余是比2^2-互模拟更好的行为等价近似。我们还引入了邻域模型的模态饱和度的概念，并研究了它与可定义性和图像有限性的关系。我们证明了一个Hennessy-Milner定理模态饱和和图像有限邻域模型。我们的主要结果是一个类似的范Benthem的特征定理和模型理论证明克雷格插值的经典模态逻辑。

In search of lost time: Axiomatising parallel composition in process algebras

This survey reviews some of the most recent achievements in the saga of the axiomatisation of parallel composition, along with some classic results. We focus on the recursion, relabelling and restriction free fragment of CCS and we discuss the solutions to three problems that were open for many years. The first problem concerns the status of Bergstra and Klop's auxiliary operators left merge and communication merge in the finite axiomatisation of parallel composition modulo bisimiliarity: We argue that, under some natural assumptions, the addition of a single auxiliary binary operator to CCS d…

树的CCS

CCS for Trees

CCS可以被认为是有限状态自动机的最自然的扩展，其中由于并行组合而使得交互成为可能。我们在这里提出了一个类似的自顶向下树自动机的扩展。我们引入了一个并行组合，这是由一个图的顶点，其中子进程位于参数化。通信只允许在图中的边所关联的子进程之间进行。我们定义了一个观察等价的基础上倒钩以及弱双相似等价，并证明了这两个概念的充分性定理。

量子双模拟经由杠铃与上下文：抑制非确定性观察者的力量

Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-Deterministic Observers

本文提出线性量子CCS演算，通过细化操作语义限制上下文不可行的非确定性选择，得到更粗且适合量子设置的双模拟，兼具提升量子态不可区分性至进程分布及保留经典信息非确定性表达力两大特性。

收缩的唯一解、CCS及其HOL形式化

Unique Solutions of Contractions, CCS, and their HOL Formalisation

收缩的唯一解是一种双相似性的证明技术，它克服了米尔纳的“方程的唯一解”技术的某些语法限制。本文概述了一个相当全面的形式化的核心理论CCS的HOL定理证明（HOL4），重点对理论的唯一解决方案的收缩。(The形式化由大约20，000行标准ML的证明脚本组成。理论本身的一些改进。特别是，我们删除的限制总和，这必须是弱保护，通过移动到根收缩，也就是说，包含在收缩预序的coarthorough precongruence。

The Zhou Ordinal of Labelled Markov Processes over Separable Spaces

There exist two notions of equivalence of behavior between states of a Labelled Markov Process (LMP): state bisimilarity and event bisimilarity. The first one can be considered as an appropriate generalization to continuous spaces of Larsen and Skou's probabilistic bisimilarity, while the second one is characterized by a natural logic. C. Zhou expressed state bisimilarity as the greatest fixed point of an operator $\mathcal{O}$, and thus introduced an ordinal measure of the discrepancy between it and event bisimilarity. We call this ordinal the "Zhou ordinal" of $\mathbb{S}$, $\mathfrak{Z}(\ma…

概率互模拟的逻辑、度量和数学特征

Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation

概率过程的许多行为等价或前序都涉及提升操作，该操作将状态关系转换为状态分布关系。我们表明，现有的几个建议，提升关系可以调和到本质上相同的提升操作的不同介绍。更有趣的是，这种提升操作很好地对应于康托洛维奇度量，这是数学中用于将状态度量提升为状态分布度量的基本概念，此外，提升操作与优化理论中的最大流问题有关。提升操作产生了一个整洁的概念，概率互模拟，我们提供逻辑，度量和算法特征。具体来说，我们扩展了Hennessy-Milner逻辑和模态μ演算与一个新的模态，从而在一个足够的概率双相似性和表达逻辑，分别。提升操作和Kantorovich度量的对应关系导致了互模拟作为伪度量的自然特征，伪度量是单调函数的后不动点。我们还提出了一个“在飞”算法来检查是否在有限系统中的两个状态相关的概率双相似性，利用提升操作和最大流问题之间的密切关系。

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

On Barbs and Labels in Reactive Systems

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

带路径上关系的模态逻辑：通过共单子语义的理论发展

Modal Logic with Relations over Paths: a Theoretical Development through Comonadic Semantics

本研究提出路径谓词模态逻辑PPML，通过共单子语义建立其模型论性质，关联DataGL等数据感知逻辑与基本模态逻辑，实现多项式时间归约。

通过一阶转移系统实现高阶语言的模块化余归纳 up-to 技术

Modular coinduction up-to for higher-order languages via first-order transition systems

本文通过完全抽象翻译将一阶LTS上的up-to双模拟技术推广到高阶语言（π-演算、λ-演算及带引用的λ-演算），仅需手动验证新语言特有技术的相容性。