基于双模拟的GSOS语言方程有效性证明方法

具有定量方面的非确定性过程的结构操作语义

Structural operational semantics for non-deterministic processes with quantitative aspects

一般框架最近已被提出作为过程的统一理论结合非确定性与定量方面（如概率或随机定时执行），旨在提供一般的结果和工具。本文在这方面提供了两个贡献。首先，我们提出了一个通用的GSOS规范格式和相应的概念互模拟的非确定性过程的定量方面。这些规范根据ULTraS模型定义了带标签的转换系统，ULTraS模型是通常的LTS的扩展，其中转换关系将任何源状态和转换标签与状态可达性权重函数（例如，概率分布）。该格式因此被称为权重函数GSOS（WF-GSOS），覆盖许多已知系统及其互模拟（例如PEPA、TIPP、PCSP）和GSOS格式（例如GSOS、加权GSOS、Segala-GSOS等）。第二个贡献是这些系统作为一类函子的余代数的特征，参数的重量结构。这一结果使我们能够证明的WF-GSOS规范格式的合理性和完整性，这些规范所引起的双相似性总是同余。

GSOS用于具有定量方面的非确定性过程

GSOS for non-deterministic processes with quantitative aspects

最近，一些通用框架已被提出作为统一的理论，结合非确定性与定量方面（如概率或随机定时执行）的过程，旨在提供一般的结果和工具。本文在这方面提供了两个贡献。首先，我们提出了一个通用的GSOS规范格式（和相应的互模拟概念）的非确定性过程的定量方面。这些规范根据ULTraS模型定义了带标签的转换系统，ULTraS模型是通常的LTS的扩展，其中转换关系将任何源状态和转换标签与状态可达性权重函数（例如，概率分布）。该格式因此被称为权重函数SOS（WFSOS），覆盖许多已知系统及其互模拟（例如PEPA、TIPP、PCSP）和GSOS格式（例如GSOS、加权GSOS、Segala-GSOS等）。第二个贡献是这些系统作为一类函子的余代数的特征，参数的重量结构。这一结果使我们能够证明的WFSOS规范格式的合理性，这些规范引起的双相似性总是同余。

Bisimilarity of Open Terms in Stream GSOS

Stream GSOS is a specification format for operations and calculi on infinite sequences. The notion of bisimilarity provides a canonical proof technique for equivalence of closed terms in such specifications. In this paper, we focus on open terms, which may contain variables, and which are equivalent whenever they denote the same stream for every possible instantiation of the variables. Our main contribution is to capture equivalence of open terms as bisimilarity on certain Mealy machines, providing a concrete proof technique. Moreover, we introduce an enhancement of this technique, called bisi…

Proving Continuity of Coinductive Global Bisimulation Distances: A Never Ending Story

We have developed a notion of global bisimulation distance between processes which goes somehow beyond the notions of bisimulation distance already existing in the literature, mainly based on bisimulation games. Our proposal is based on the cost of transformations: how much we need to modify one of the compared processes to obtain the other. Our original definition only covered finite processes, but a coinductive approach allows us to extend it to cover infinite but finitary trees. After having shown many interesting properties of our distance, it was our intention to prove continuity with res…

Proving Linearizability via Branching Bisimulation

Linearizability and progress properties are key correctness notions for concurrent objects. However, model checking linearizability has suffered from the PSPACE-hardness of the trace inclusion problem. This paper proposes to exploit branching bisimulation, a fundamental semantic equivalence relation developed for process algebras which can be computed efficiently, in checking these properties. A quotient construction is provided which results in huge state space reductions. We confirm the advantages of the proposed approach on more than a dozen benchmark problems.

证明行为分离性

Proving Behavioural Apartness

针对余代数互模拟性证明的局限性，提出通过对偶行为等价定义行为分离性，在子分布函子等系统中将无限量化转化为有限规则，并提供优化证明规则及示例验证。