### 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.

### License

BSD License

### Topics

- Computer science/Automata and formal languages
- Mathematics/Algebra

### Session C2KA_DistributedSystems

- Stimuli
- CKA
- C2KA
- Topology_C2KA
- Communication_C2KA

## Cite

×

C2KA_DistributedSystems-AFP

    @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   = {August},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/C2KA_DistributedSystems.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Aug 6, 2019 : Isabelle2019