Extensions to Temporal Logic

There have been some attempts to introduce further temporal operators. Most of these more or less elaborate ways of expressing different temporal structures and are often a shorthand way of denoting combinations the basic four temporal operators. This section will introduce some of these temporal operators. These operators are outside the scope of the present work - but will be described to the sake of completeness. One example is the concept of "now":

• 136#136 7#7 is 137#137 now.

Another set of operators are the binary operators that are introduced in (Kamp, 1968).

• 138#138 133#133 has been 137#137 since a time when 7#7 was 137#137.

• 139#139 133#133 will be 137#137 until a time when 7#7 is 137#137.

Interesting enough then the following equations holds:

140#140

141#141

Regarding the two operators (Galton, 1999) notes the following:

The importance of the S and U operators is that they are expressively complete with respect to first-order temporal properties on continuous, strictly linear temporal orders (which is not true for the one-place operators on their own).

As noted in the beginning of this chapter then these operators are only displayed here for the sake of completeness. The application of these operators are common in Computation Tree Logic* (CTL*). A more elaborate discussion can be found in (Penczek, 1991).