Technical Report CS0505

Title: Interleaving Set Temporal Logic
Authors: Shmuel Katz and Doron Peled
Abstract: A new temporal logic and interpretation are suggested which have features from linear temporallogic, branching time temporal logic, and partial order temporal logic. The new logic can describe properties essential to the specification and correctness proofs of distributed algorithms such as those for global snapshots. It is also appropriate for the justification of proof rules and ascribing temporal semantics to properties such as layering of a program. These properties cannot be described with existing temporal logics. The semantic model of the logic is based on a collection of sets of interleaving sequences which reflect partial orders from the underlying semantics of the computational model. For the common partial order derived from sequentiality in execution of each process, the logic will distinguish between nondeterminism due to the parallel execution and nondeterminism due to local nondeterministic choices. The difference in expressive power is thus qualitative, and not merely due to the presence or absence of a particular temporal operator. In the logic. theorems are proven which clarify when it is possible to establish a property P for some of the interleaving computations, and yet conclude the truth of P for every interleaving.
CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (, rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the CS technical reports of 1988
To the main CS technical reports page

Computer science department, Technion