Specification of distributed programs using temporal interval logic

Temporal logic has been suggested as an appropriate language for the specification and verification of distributed algorithms. However, temporal logic is too low level because it requires the user to specify specific state changes. To encourage a more abstract level of formalism, temporal interval logic (TIL) has been proposed as an extension of temporal logic. An adequate base from which to evaluate TIL should consist of several specifications written in TIL, a suitable proof theory for TIL, a decision procedure for TIL and an analysis of the complexity of the decision procedure. The finite model property of propositional temporal logic suggest that programs may be synthesized directly from temporal specifications. Therefore, advantages of disadvantages that TIL brings to the synthesis of programs need to be explored. This thesis presents the following results: (a) A symmetric and distributed synchronization scheme for communicating processes superior to other distributed schemes in that it is symmetric in its treatment of input and output commands, and in that its performance is equivalent to the best previously known schemes. (b) A formal specification of the scheme in temporal interval logic and verification of the properties of the scheme in the framework of the logic. (c) A polynomial space and time scheme for translating formulas in TIL to PTL. This, together with Sistla and Clarke's result that the decision procedure for PTL is PSPACE complete, establishes that TIL is PSPACE complete. (d) A proof that several sets of temporal logic operators are equivalent. This is accomplished by introducing auxiliary variables and the notion of...