We formalise the modal operators from the concurrent dynamic logics of Peleg, Nerode and Wijesekera in a multirelational algebraic language based on relation algebra and power allegories, using relational approximation operators on multirelations developed in a companion article. We relate Nerode and Wijesekera's box operator with a relational approximation operator for multirelations and two related operators that approximate multirelations by different kinds of deterministic multirelations. We provide an algebraic soundness proof of Goldblatt's axioms for concurrent dynamic logic as an application.

翻译：本文基于关系代数与幂类象理论，采用姊妹篇中发展的多关系关系近似算子，以多关系代数语言形式化Peleg、Nerode和Wijesekera并发动态逻辑中的模态算子。我们将Nerode与Wijesekera的盒算子与多关系的关系近似算子相关联，并建立两个相关算子——它们通过不同类型的确定性多关系对多关系进行近似。作为应用，我们给出Goldblatt并发动态逻辑公理的代数正确性证明。