TY - GEN

T1 - Specifying message passing systems requires extending temporal logic

AU - Koymans, R.L.C.

PY - 1989

Y1 - 1989

N2 - 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.

AB - 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.

U2 - 10.1007/3-540-51803-7_28

DO - 10.1007/3-540-51803-7_28

M3 - Conference contribution

SN - 3-540-51803-7

SN - 978-3-540-51803-7

T3 - Lecture Notes in Computer Science (LNCS)

SP - 213

EP - 223

BT - Temporal logic in specification

A2 - Banieqbal, B.

A2 - Barringer, H.

A2 - Pnueli, A.

PB - Springer

CY - Berlin

ER -