Specifying message passing systems requires extending temporal logic

R.L.C. Koymans

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

6 Citations (Scopus)

Abstract

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.
Original languageEnglish
Title of host publicationTemporal logic in specification
Subtitle of host publicationAltrincham, UK, April 8-10, 1987, Proceedings
EditorsB. Banieqbal, H. Barringer, A. Pnueli
Place of PublicationBerlin
PublisherSpringer
Chapter28
Pages213-223
Number of pages11
ISBN (Electronic)978-3-540-46811-0
ISBN (Print)3-540-51803-7, 978-3-540-51803-7
DOIs
Publication statusPublished - 1989

Publication series

NameLecture Notes in Computer Science (LNCS)
Volume398
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint Dive into the research topics of 'Specifying message passing systems requires extending temporal logic'. Together they form a unique fingerprint.

Cite this