A Relational Model for Temporal Logic

We use Tarski's relational calculus to construct a model of linear temporal logic. Both discrete and dense time are covered and we obtain denotational domains for a large variety of reactive systems. Keywords: Relational algebra, reactive systems, temporal algebra, temporal logic. 1 Introduction The relational calculus has been very successful for modelling possibly non-deterministic systems provided they can be fully described in terms of their initial and final states. In contrast, the linear temporal logic (LTL) of Manna and Pnueli was designed for describing properties of reactive systems, where the behaviour between initiation and termination is also important. Unlike the calculus of relations, LTL has no operator for sequential composition. Therefore the standard model of LTL is unsuitable as a semantic domain for programs: LTL formulae describe properties of executions, but they are not themselves programs. Program constructs and temporal connectives cannot be mixed. This is ve..