The concurrent refinement algebra has been developed to support rely/guarantee reasoning about concurrent programs. The algebra supports atomic commands and defines parallel composition as a synchronous operation, as in Milner's SCCS. In order to allow specifications to be combined, the algebra also provides a weak conjunction operation, which is also a synchronous operation that shares many properties with parallel composition. The three main operations, sequential composition, parallel composition and weak conjunction, all respect a (weak) quantale structure over a lattice of commands. Further structure involves combinations of pairs of these operations: sequential/parallel, sequential/weak conjunction and parallel/weak conjunction, each pair satisfying a weak interchange law similar to Concurrent Kleene Algebra. Each of these pairs satisfies a common biquantale structure. Additional structure is added via compatible sets of commands, including tests, atomic commands and pseudo-atomic commands. These allow stronger (equality) interchange and distributive laws. This paper describes the result of restructuring the algebra to better exploit these commonalities. The algebra is implemented in Isabelle/HOL.

翻译：并发精化代数旨在支持对并发程序进行依赖/保证推理。该代数支持原子命令，并将并行组合定义为同步操作，类似于Milner的SCCS。为允许规约的组合，该代数还提供了弱合取操作，这也是一种与并行组合共享诸多性质的同步操作。三种主要操作——顺序组合、并行组合和弱合取——均在命令格结构上满足（弱）quantale结构。进一步的结构涉及这些操作的成对组合：顺序/并行、顺序/弱合取以及并行/弱合取，每对均满足类似于并发Kleene代数的弱交换律。每对组合均构成共同的biquantale结构。通过兼容命令集（包括测试、原子命令和伪原子命令）可添加附加结构，从而强化（等式）交换律和分配律。本文描述了重构该代数以更好利用这些共性的结果。该代数已在Isabelle/HOL中实现。