Hostname: page-component-7c8c6479df-hgkh8 Total loading time: 0 Render date: 2024-03-29T01:14:13.794Z Has data issue: false hasContentIssue false

Temporal algebra

Published online by Cambridge University Press:  01 June 1998

BURGHARD von KARGER
Affiliation:
Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel, Preusserstraßer 1–9, D-24105 Kiel, Germany

Abstract

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, namely that ([oplus ], &[ominus ]tilde;) is a Galois connection and that ([ominus ], [oplus ]) is a perfect Galois connection. 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.

Type
Research Article
Copyright
1998 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)