Furusawa and Struth construct an algebra of multirelations (where an element is related to a set of elements) motivated by Peleg’s concurrent dynamic logic [1]. Sequential composition is no longer associative and interacts with parallel composition through a weak distributive law. The authors’ aim appears to be to allow specialization to alternation and concurrency; the presentation is kept very general.

They point out that communication aspects are not modeled. Differences with Parikh’s game logic [2] are discussed. Special cases of distributive lattices and Boolean algebras are studied, and modal operators are also considered. Algebraic variants of Peleg’s axioms are shown to be sound. Several results have been verified formally with the theorem prover Isabelle/HOL. It will be interesting to see how the authors develop this work from the point of view of applications.