von Karger, Burghard Temporal algebra. (English) Zbl 0917.03011 Math. Struct. Comput. Sci. 8, No. 3, 277-320 (1998). 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”. Reviewer: J.Šefránek (Bratislava) Cited in 1 ReviewCited in 18 Documents MSC: 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.) Keywords:temporal algebra; temporal logic; complete lattice; Galois connection; fixed point; linear temporal logic; branching time logic CTL; intuitionistic temporal logic; graph-theoretic algorithm; algebraic reasoning; temporal reasoning PDFBibTeX XMLCite \textit{B. von Karger}, Math. Struct. Comput. Sci. 8, No. 3, 277--320 (1998; Zbl 0917.03011) Full Text: DOI