A logical characterization of asynchronously communicating agents

Abstract

In this paper we study the behaviour of distributed systems. We consider systems composed of a fixed number of sequential processes communicating by asynchronous message passing. The behaviour is represented by a subclass of partial orders called asynchronously communicating agent structures, abbreviated ACA structures.

We present a logical characterization of ACA structures in the framework of temporal logic.

The modalities of the logic capture the concepts of communication, concurrency and locality.

We define an axiomatic basis for the logic and show both soundness and completeness.