A logical characterization of asynchronously communicating agents

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.