Partially Observable Concurrent Kleene Algebra

Kleene Algebra with Observations

Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Generalising KAT to reason about concurrent programs is not straightforward, because axioms native to KAT in conjunction with expected axioms for concurrency lead to an anomalous equation. In this paper, we propose Kleene algebra with observations (KAO), a variant of KAT, as an alternative foundation for extending KAT to a concurrent setting. We characterise the free model of KAO, and establish a decision procedure w.r.t. its equational theory.

关于部分可加Kleene代数

On Partially Additive Kleene Algebras

我们定义了部分加性Kleene代数的概念，这是一个Kleene代数，其中+运算只需要部分定义。这些结构形式化了许多不能直接用Kleene代数处理的例子。我们与部分加性Kleene代数现有的代数结构，展示与Kleene代数，部分加性范畴，闭半环的范畴连接。

Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra

Concurrent Kleene Algebra is an elegant tool for equational reasoning about concurrent programs. An important feature of concurrent programs that is missing from CKA is the ability to restrict legal interleavings. To remedy this we extend the standard model of CKA, namely pomsets, with a new feature, called boxes, which can specify that part of the system is protected from outside interference. We study the algebraic properties of this new model. Another drawback of CKA is that the language used for expressing properties of programs is the same as that which is used to express programs themsel…

广义莫比乌斯范畴与卷积克里勒代数

Generalised Möbius Categories and Convolution Kleene Algebras

本文提出广义莫比乌斯范畴与经典星定义的结合，用于构建卷积克里勒代数，应用于程序验证和高维重写中的代数推理。

并发动态代数

Concurrent Dynamic Algebra

我们重建Peleg的并发动态逻辑的背景下，模态Kleene代数。我们探讨了其多关系语义的代数结构，并从这个基础上发展了并发动态代数的抽象公理化。在这种公理化中，顺序复合不是结合的。它通过弱分配律与并发合成相互作用。并发动态代数的模态算子是从域和反域算子的抽象公理中得到的; Kleene星被建模为最小不动点。Peleg公理的代数变体在这些代数中是有效的，并且证明了它们的可靠性相对于多关系模型。其他结果包括迭代原则的Kleene星和反驳的变种Segerberg的公理在multisolational设置。最重要的结果已正式与伊莎贝尔/HOL验证。

Convolution and Concurrency

We show how concurrent quantales and concurrent Kleene algebras arise as convolution algebras $Q^X$ of functions from structures $X$ with two ternary relations that satisfy relational interchange laws into concurrent quantales or Kleene algebras $Q$. The elements of $Q$ can be understood as weights; the case $Q=\bool$ corresponds to a powerset lifting. We develop a correspondence theory between relational properties in $X$ and algebraic properties in $Q$ and $Q^X$ in the sense of modal and substructural logics, and boolean algebras with operators. As examples, we construct the concurrent quant…

代数相干合流与高阶球形克莱尼代数

Algebraic coherent confluence and higher globular Kleene algebras

本文提出高阶球形克莱尼代数，将合流形式化扩展至相干合流证明，通过等式推理得到相干Church-Rosser定理与Newman引理，并应用于多面图建模的高阶重写系统。

非确定性迭代与测试的统一范畴论视角

A Unifying Categorical View of Nondeterministic Iteration and Tests

本文从范畴论视角分离并分析Kleene迭代，提出含余积与测试的Kleene迭代范畴，证明其兼容异常、存储、并发等特性，并将自由模型刻画为非确定性有理树。

概率信赖担保演算

Probabilistic Rely-guarantee Calculus

Jones的可靠保证演算共享变量并发扩展到包括概率行为。我们使用的代数方法，结合和适应概率Kleene代数并发Kleene代数。稳健的代数相对于一般的概率事件结构语义。本文的主要贡献是建立在语义之上的可靠保证规则的集合。特别是，我们展示了如何获得的概率范围内的真实并发指称语义的可靠保证规则。这些规则的使用说明了一个简单的概率并发程序的详细验证：一个错误的Eratosthenes筛。

带测试的有限加权Kleene代数的完备性

Completeness of Finitely Weighted Kleene Algebra With Tests

本研究在已有有限加权Kleene代数完备性结论基础上，新增整性假设，建立带测试的有限加权Kleene代数的关系与语言完备性，为带权重上界的加权程序等式推理提供天然框架。

并发的本质

The Nature of Concurrency

本研究基于真并发进程代数的最新成果，阐明交错并发与真并发的关系，给出事件结构、Petri网等真并发模型的进程代数基础。

Automated Verification of Reactive and Concurrent Programs by Calculation

Reactive programs combine traditional sequential programming constructs with primitives to allow communication with other concurrent agents. They are ubiquitous in modern applications, ranging from components systems and web services, to cyber-physical systems and autonomous robots. In this paper, we present an algebraic verification strategy for concurrent reactive programs, with a large or infinite state space. We define novel operators to characterise interactions and state updates, and an associated equational theory. With this we can calculate a reactive program's denotational semantics, …

在并发细化代数中推理分配律

Reasoning about distributive laws in a concurrent refinement algebra

本文聚焦并发细化代数，通过支持有限与无限行为实现完全正确性，提出并证明了作为等式的强分配律，用于分配 rely/guarantee 命令并处理并发程序的数据细化。

重构一种并发精化代数

Restructuring a concurrent refinement algebra

本文重构支持 rely/guarantee 推理的并发精化代数，统一其 quantale/biquantale 结构并强化交换与分配性质，且在 Isabelle/HOL 中实现。

带有假设的连续代数

Continuous Algebras with Hypotheses

本文提出一个统一的框架，涵盖Kleene代数的各种变体以及正则树语言，通过考虑由完全格有序的代数，其中可以计算最小固定点，并提供一个由封闭语言组成的标准模型，证明其在所有连续模型上都是正确且完整的。此外，本文研究了准等式公理化，并展示了如何通过模块化的方式获得完整公理化，从而在每个情况下证明了交换Kleene代数、bi-KA和正则树语言在不同假设下的完备性。

面向对象并发模型的实用图验证

Towards Practical Graph-Based Verification for an Object-Oriented Concurrency Model

为了利用多核和分布式平台的强大功能，并使软件工程师更容易开发并发软件，已经提出了不同的面向对象的并发模型，如SCOOP。尽管分析SCOOP程序的实际重要性，目前还没有通用的验证方法，直接对程序代码进行操作，而无需额外的注释。其中一个原因是SCOOP的大量部分冲突的语义形式化（无论是在理论上还是在实现上）。在这里，我们提出了一个简单的图形转换系统（GTS）为SCOOP的运行时语义，掌握所有已知的语义语言的最常见的功能。这个运行时模型是在最先进的GTS工具GROOVE中实现的，它使我们能够模拟，分析和验证SCOOP程序的一个子集的死锁和其他行为属性。除了提出第一种方法来验证SCOOP程序的自动翻译GTS，我们还强调我们的经验，应用GTS（特别是GROOVE）指定语义的形式，运行时模型，这应该是转移到GTS模型的其他并发语言和库。