We prove that it is impossible to express asynchronous message passing within the framework of first-order temporal logic with both future and past operators (as studied by Kamp).This is an extension of a result of Sistla et al. that unbounded buffers cannot be expressed in linear time temporal logic.Although strengthening Kamp's logic by adding counting and quantification over occurrences of propositions enables the expression of most message passing systems, we argue that order preserving systems which may lose messages still remain inexpressible.This is caused by the impossibility to couple each message that is delivered by a message passing system id a unique message accepted 6y that system.These results seem to necessitate the enrichment of TL-based formalisms, e.g. with auxiliary data structures or histories as done, respectively, by Lamport and Hailpern.Observe that Lamport employs a hybrid formalism (TE + Data Structures), and that in Hailpern's method similar systems, such as FIFO and LIFO.do not have similar specifications.We shall prove that no such enrichment is logically required.This is done by introducing an assumption which makes the unique coupling mentioned above possible.This assumption can be formulated in TL.In this way, no extraneous formalisms are introduced, and both FIFO and LIFO are expressible with equal ease.

This paper indicates a method of describing real-time processes and their asynchronous communication by means of message exchanges. This description method is based upon an extension of linear time temporal logic to a special temporal logic in which real-time and asynchronous message passing properties can be expressed. We give a model of this logic, define new operators and show amongst others how they can be applied to specify real-time asynchronous message passing and an abstract real-time transmission medium.