Concurrent Dynamic Algebra

TL;DR

This paper develops an algebraic framework for concurrent dynamic logic within modal Kleene algebras, introducing new axioms and proving soundness and iteration principles, with formal verification in Isabelle/HOL.

Contribution

It reconstructs Peleg's concurrent dynamic logic algebraically, allowing for non-associative composition and providing a formal basis with soundness proofs and iteration principles.

Findings

Algebraic axioms valid in multirelational models.

Soundness of algebraic variants of Peleg's axioms.

Formal verification of key results using Isabelle/HOL.

Abstract

We reconstruct Peleg's concurrent dynamic logic in the context of modal Kleene algebras. We explore the algebraic structure of its multirelational semantics and develop an abstract axiomatisation of concurrent dynamic algebras from that basis. In this axiomatisation, sequential composition is not associative. It interacts with concurrent composition through a weak distributivity law. The modal operators of concurrent dynamic algebra are obtained from abstract axioms for domain and antidomain operators; the Kleene star is modelled as a least fixpoint. Algebraic variants of Peleg's axioms are shown to be valid in these algebras and their soundness is proved relative to the multirelational model. Additional results include iteration principles for the Kleene star and a refutation of variants of Segerberg's axiom in the multirelational setting. The most important results have been verified formally with Isabelle/HOL.