Temporal logic studies the structure or topology of time
[13]. It uses special operators such as 
(``henceforth'') and 
(``eventually'') to describe the temporal
connectives that occur in language. In more recent years, temporal logic
has been successfully applied in various areas of computer science,
especially software verification. (See for example [3],
[2], [18].) Ostroff uses Real Time
Temporal Logic (RTTL) in describing the specifications for purposes
of controller synthesis. RTTL is an extension of the Manna-Pnueli temporal
logic [11]. It uses the standard temporal operators and
adds the proof rules needed for real-time properties. The following
summary follows closely that presented in [14]. The
reader is referred to [15] for more details on RTTL.
A state-formula is any first order predicate which does not
contain any temporal operators. If a state-formula 
evaluates
to true in state s, we write 
.
Unlike a state-formula which can be evaluated in a single state, a
temporal-formula can only be evaluated over a sequence of
states, or trajectory, which is given by 
The k-shifted trajectory suffix is then given by
The symbol
means that the trajectory 
satisfies the formula w.
We will be concerned with two basic temporal operators: 
(``next'') and 
(``until''). From these, operators such
as (``eventually''), (``henceforth''), 
(``precedes''), and others, can be derived.
With the two basic operators defined above (``next'' and ``until''), we can derive other operators as follows:
(``eventually w holds in some state'') can be
rewritten as 
.
(``henceforth w holds in all states'') can be
rewritten as 
.
(`` 
precedes 
whenever
occurs'') can be rewritten as 
.
Thus, in Ostroff's method, the specification model 
consists of a
set of temporal formulae. See Sections 6.2 and 7.2 for examples of
specifications expressed in Temporal Logic.