ON THE SATISFIABILITY PROBLEM FOR LAMPORT'S PROPOSITIONAL TEMPORAL LOGIC OF ACTIONS AND SOME OF ITS EXTENSIONS

Abstract

The Temporal Logic of Actions (TLA) devised by Lamport is a logic for proving the correctness of concurrent systems. A distinctive feature of the logic is the use of “action formulae” to encode the “before-after” behaviour of transitions, a feature that is especially suitable for Lamport's transition-axiom method. Abadi has given a complete axiomatization for the propositional fragment of this logic, and conjectured that its validity problem may be in PSPACE. In this paper we confirm that conjecture. In fact we show that the validity problem for TLA is PSPACE-complete. For this we give a space-optimal automata-theoretic decision procedure for TLA. Our result is obtained with respect to a logic which is a conservative extension of Lamport's TLA. Thus our decision procedure applies to the more restricted logic. We show how the automata-theoretic framework handles abstraction, as used in TLA, a feature considered useful for hierarchical and compositional reasoning.