Concurrent dynamic algebra

DOI10.1145/2785967MaRDI QIDQ5277895zbMATH OpenOpenAlexFDO

Authors Hitoshi Furusawa, Georg Struth

Publication date 12 July 2017

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1407.5819

zbMATH Keywords

dynamic logicmodal algebramultirelations

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Other algebras related to logic (03G25) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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.

Recommendations

• Concurrent algebras: an algebraic study of a fragment of concurrent propositional dynamic logic
• Concurrent Kleene Algebra
• Concurrent Kleene algebra and its foundations
• Parallel action: Concurrent dynamic logic with independent modalities
• Foundations of concurrent Kleene algebra

Cites work

• A completeness theorem for Kleene algebras and the algebra of regular events
• Alternation
• Communication in concurrent dynamic logic
• Concurrent dynamic logic
• Domain Axioms for a Family of Near-Semirings
• Dynamic algebras with test
• Dynamic algebras: Examples, constructions, applications
• scientific article; zbMATH DE number 3880483 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• Internal axioms for domain semirings
• Isabelle/HOL. A proof assistant for higher-order logic
• Kleene algebra with domain
• Modal logic
• Modelling angelic and demonic nondeterminism with multirelations
• Modelling simultaneous games in dynamic logic
• Monotone Predicate Transformers as Up-Closed Multirelations
• Multirelational models of lazy, monodic tree, and probabilistic Kleene algebras
• On equations for regular languages, finite automata, and sequential networks
• Parallel action: Concurrent dynamic logic with independent modalities
• Refinement Calculus
• Relation algebras
• Tableaux for constructive concurrent dynamic logic
• The cube of Kleene algebras and the triangular prism of multirelations
• Theory and Applications of Relational Structures as Knowledge Instruments

Cited in

(13)

• Parallel action: Concurrent dynamic logic with independent modalities
• A semantics and a logic for \textit{Fuzzy Arden Syntax}
• Kleisli, Parikh and Peleg compositions and liftings for multirelations
• A relation-algebraic approach to multirelations and predicate transformers
• Hoare semigroups
• Generating Posets Beyond N
• An algebraic approach to multirelations and their properties
• Taming multirelations
• Concurrent algebras: an algebraic study of a fragment of concurrent propositional dynamic logic
• Determinism of multirelations
• Single-set cubical categories and their formalisation with a proof assistant
• On the inner structure of multirelations
• Modal algebra of multirelations

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: Concurrent dynamic algebra

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5277895)