Temporal Logic of Programs

Important goals of mathematical logic are, in general, to:

Let us begin with an informal discussion of the basic ideas already indicated in the introduction. The starting point of our considerations is the idea that there are different time points which may yield different truth values of propositions. We make a first important agreement: we assume the set of time points to be infinite, discrete and linearly ordered with a smallest element. This leads to the following picture of a time scale:

Temporal logic can be developed from its propositional basis to a first-order predicate logic in a way analogous to how this is done in the classical case.

We want to apply temporal logic to the description of (the computational behaviour of) programs and their verification. For the sake of technical conciseness we restrict the programs to a fixed (somewhat abstract) syntactic form.

Let be a program. We begin with the consideration of invariance properties whose general form is

We now want to investigate the verification of eventuality properties of programs expressing that “eventually something will happen”. However, we first have to come back to our interleaving model of computation and the notion of execution sequences of programs and have a somewhat closer look at them.

All proof principles discussed in the previous sections are applicable to any program. For sequential programs there exist two further special verification methods which — although related to the universal methods — have some significance of their own and are sometimes easier to use. In this last chapter we want to represent these two methods within our temporal logic framework.