Specifying message passing systems requires extending temporal logic

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. In our analysis the source of this inexpressiveness is the impossibility to couple each message that is delivered by a message passing system to auniquemessage accepted by that system. This result seems 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 (TL+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 additional axiom within TL which formalizes the assumption that messages accepted by the system can be uniquely identified. In this way, no extraneous formalisms are introduced, and both FIFO and LIFO are expressible with equal ease.