SRC Research Report 65
SRC Research Report 65Lamport recently invented a temporal logic of actions suitable for expressing concurrent programs and for reasoning about their computations. In this logic, actions have syntactic representations, which can be combined and analyzed. The basic construct for relating actions and computations is [ ]; a computation satisfies the formula [A] if either the computation has halted or the first action in the computation is an A action. In addition, the language includes the temporal operators "always" and "eventually", and thus it is easy to write both safety and liveness formulas.
However, the temporal logic of actions is not very expressive in some respects (just expressive enough). One cannot define the "next" and the "until" operators of many previous temporal logics. This is actually a feature, in that formulas with "until" are too often incomprehensible, and "next" violates the important principle of invariance under stuttering.
A proof system for the logic of actions might be obtained by translating into previous, richer formalisms. In this translation we forfeit the logic and its advantages. A new suit of rules for temporal reasoning with actions is therefore wanted. A complete axiomatization can provide some guidance in choosing and understanding the rules used in practice, and in particular the laws for reasoning about programs.
In this paper, we study a proof system for a propositional logic, PTLA. After an informal introduction, we define the syntax and semantics of PTLA precisely, and then present our proof system and prove its completeness.
Back to the SRC Research Reports main page.