Foundations of Communicating Concurrent Kleene Algebra

Communication is integral to the understanding of agent interactions in concurrent systems. In this paper, we propose a mathematical framework for communication and concurrency called Communicating Concurrent Kleene Algebra (C 2 KA). C 2 KA supports the ability to work in either a state-based or event-based model for the specification of concurrent and communicating systems by extending concurrent Kleene algebra with the notion of communication actions. This extension captures both the influence of external stimuli on agent behaviour as well as the communication and concurrency of communicating agents. We also illustrate the dierent levels of abstraction for the behaviour of agents that are oered by the proposed framework with the specification of a simple illustrative example.