Restructuring a concurrent refinement algebra
<|reference_start|>Restructuring a concurrent refinement algebra: 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.<|reference_end|>
@article{hayes2024restructuring,
    title={Restructuring a concurrent refinement algebra},
    author={Ian J. Hayes and Larissa A. Meinicke and Naso Evangelou-Oost},
    journal={arXiv preprint arXiv:2405.05690},
    year={2024},
    archivePrefix={arXiv},
    eprint={2405.05690},
    primaryClass={cs.LO}
}