An algebraic approach to temporal logic

Abstract

The sequential calculus is an algebraic calculus, intended for reasoning about phenomena with a duration and their sequencing. It can be specialized to various domains used for reasoning about programs and systems, including Tarski's calculus of binary relations, Kleene's regular expressions, Hoare's CSP and Dijkstra's regularity calculus. In this paper we use the sequential calculus as a tool for algebraizing temporal logics. We show that temporal operators are definable in terms of sequencing and we show how a specific logic may be selected by introducing additional axioms. All axioms of the complete proof system for discrete linear temporal logic (given in [9]) are obtained as theorems of sequential algebra. Our work embeds temporal logic into an algebra naturally equipped with sequencing constructs, and in which recursion is definable. This could be a first step towards a design calculus for transforming temporal specifications by stepwise refinement into executable programs. This paper is an extended abstract of a technical report [5] containing full proofs (available by ftp). Most proofs have been omitted and simplifying assumptions were made to make the presentation easier.