Temporal algebra. (English) Zbl 0917.03011

Author’s summary: “We develop temporal logic from the theory of complete lattices, Galois connections, and fixed points. In particular, we prove that all seventeen axioms of Manna and Pnueli’s sound and complete proof system for linear temporal logic can be derived from just two postulates. We also obtain a similar result for the branching time logic CTL.
A surprising insight is that most of the theory can be developed without the use of negation. In effect, we are studying intuitionistic temporal logic. Several examples of such structures occurring in computer science are given. Finally, we show temporal algebra at work in the derivation of a simple graph-theoretic algorithm.
This paper is tutorial in style and there are no difficult technical results. To the experts in temporal logics, we hope to convey the simplicity and beauty of algebraic reasoning as opposed to the machine-orientedness of logical deduction. To those familiar with the calculational approach to programming, we want to show that their methods extend easily and smoothly to temporal reasoning. For anybody else, this text may serve as a gentle introduction to both areas”.


03B45 Modal logic (including the logic of norms)
03B70 Logic in computer science
06A15 Galois correspondences, closure operators (in relation to ordered sets)
06B23 Complete lattices, completions
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI