Email Gateway (Aug 22 2022 at 20:21): Email Gateway (Aug 22 2022 at 20:21):From: Lawrence Paulson <lp15@cam.ac.uk>
We have a new entry, by Maxime Buyse and Jason Jaskolka:
Communicating Concurrent Kleene Algebra for Distributed Systems Specification
Communicating Concurrent Kleene Algebra (C²KA) is a mathematical framework for capturing the communicating and concurrent behaviour of agents in distributed systems. It extends Hoare et al.'s Concurrent Kleene Algebra (CKA) with communication actions through the notions of stimuli and shared environments. C²KA has applications in studying system-level properties of distributed systems such as safety, security, and reliability. In this work, we formalize results about C²KA and its application for distributed systems specification. We first formalize the stimulus structure and behaviour structure (CKA). Next, we combine them to formalize C²KA and its properties. Then, we formalize notions and properties related to the topology of distributed systems and the potential for communication via stimuli and via shared environments of agents, all within the algebraic setting of C²KA.
https://www.isa-afp.org/entries/C2KA_DistributedSystems.html
Looks interesting!
Larry Paulson
Last updated: Apr 20 2024 at 04:19 UTC