Contents of Real-Time Temporal Logic

Real-Time Temporal Logic

The following discussion is taken from [104]. Temporal logic has its origins in philosophy, where it was used to analyze the structure or topology of time [130]. In recent years, it has found application in computer science, especially in the areas of software verification and knowledge-based systems [30,117,70,112,69,67,28,66].

In physics and mathematics, time has traditionally been represented as just another variable. First order predicate calculus is used to reason about expressions containing the time variable, and there is thus apparently no need for a special temporal logic.

Philosophers found it useful to introduce special temporal operators, such as $\Box$ (henceforth) and $\Diamond$ (eventually), for the analysis of temporal connectives in language. The new formalism was soon seen as a potentially valuable tool for analyzing the topology of time. For example, various types of semantics can be given to the temporal operators depending on whether time is linear, parallel or branching. Another question that may be asked is whether time is discrete or continuous.

The temporal operators have been found useful for specifying program behaviour. A structure of states (e.g. a sequence or tree of states) is the key concept that makes temporal logic suitable for program specification. A formula, containing temporal logic operators, is interpreted over a structure of states.

In programming languages, the structures represent the computations executed by a program. Such a computation may be used to interpret a temporal formula. In this way, a programming language is said to be endowed with a temporal semantics.

Some of the different types of temporal semantics include:

Interval semantics [134,95,96]. The semantics is based on intervals of time, thought of as representing finite chunks of system behaviour. An interval may be divided into two contiguous subintervals, thus leading to the chop operator.
Point semantics, in which temporal formulas are interpreted as requiring some system behaviour with respect to a certain reference point in time. Past operators refer to the time prior to the reference point. Future operators refer to the time after the reference point. Obviously, a point cannot be divided, and there is thus no simple definition of a chop operator.
Point semantics may be further divided³ into three classes.
- Linear semantics [83,120,81]. In linear semantics, each moment has only one possible future corresponding to the history of the development of the system.
- Branching semantics [25,20]. In branching time semantics, time has a tree-like nature in which, at each instant, time may split into alternative courses representing different choices made by a system.
- Partial order semantics. Partial order semantics has been explored only recently. The reader is referred to [81] and other articles in the same volume as [81] for further information.

Once the type of structure to be used for interpreting temporal formulas is selected, there is still a further decision to be made. How are the structures to represent program executions or computations? There are at least two possibilities.

Maximal parallelism [52,62]. The number of instructions in concurrent processes that can be executed simultaneously is maximized. Thus, two processes are never both waiting to achieve a shared communication.
Interleaved executions. Concurrent activity of two parallel processes is represented by interleaving their atomic actions [82]. Fairness and time bound constraints are then used to exclude inappropriate interleavings (e.g. a sequence in which an enabled action is never executed).

The various temporal logics can be used to reason about qualitative temporal properties. Safety properties that can be specified include mutual exclusion and absence of deadlock. Liveness properties include termination and responsiveness. Fairness properties include scheduling a given process infinitely often, or requiring that a continuously enabled transition ultimately fire.

Various proof systems and decision procedures for finite state systems can be used to check the correctness of a program or system.

In real-time temporal logics, quantitative properties can also be expressed such as periodicity, real-time response (deadlines), and delays. Early approaches to real-time temporal logics were reported in [10,63,111]. Since then, real-time temporal logics have been explored in great detail.

Subsections