# Communicating Concurrent Kleene Algebra for Distributed Systems Specification

 Title: Communicating Concurrent Kleene Algebra for Distributed Systems Specification Authors: Maxime Buyse (maxime /dot/ buyse /at/ polytechnique /dot/ edu) and Jason Jaskolka Submission date: 2019-08-06 Abstract: 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. BibTeX: @article{C2KA_DistributedSystems-AFP, author = {Maxime Buyse and Jason Jaskolka}, title = {Communicating Concurrent Kleene Algebra for Distributed Systems Specification}, journal = {Archive of Formal Proofs}, month = aug, year = 2019, note = {\url{https://isa-afp.org/entries/C2KA_DistributedSystems.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.