A straightforward extension of leads to what Thayse 1989 calls
**linear-time temporal logic**, which is not only
useful in AI for modeling domains that
include phenomena that vary with time (and what robust
domain fails to include such phenomena?)
but is also a tool
for verifying the behavior of computer programs that have nothing to do with
AI.
The extension comes via two new operators,
and ; this yields a total of
four operators now, which are read as follows:

- - at the next time
- - always
- - eventually
- - until

(The quantifier essentially says `there is
exactly one *x* such that'.)
Now, using *P* again as the set of all atomic wffs from the propositional
calculus, define a function *I* analogously to *V* from above; specifically, let *I*
be a mapping from to the truth-values `true' and `false', {**T**,
**F**}. (*I* tells us whether or not
a given atomic formula *p* is true at a given state *s*.)
A **temporal interpretation** is then a pair *I*)
that can give precise ``meaning'' to expressions in the logic, as follows.
For the propositional case, a conjunction is true at a state *s*
iff both *p* and *q* are true at *s*. This is written as iff and . For the interesting
cases, the operators, we let denote the (*i*+1)st member of the
sequence

Then, for example,

- =
**T**iff =**T**, and - =
**T**iff =**T**,

We should mention
that temporal logic is by no means the only tool used in AI for
enabling reasoning about time and change. In fact, AI has often tended to
refer to the entities posited in temporal logic (e.g., events, possible worlds,
or histories) directly in modifications of . The earliest such
formalism was the **situation calculus**, invented by John McCarthy (1968);
a good presentation of this formalism, modernized
from the form it had when first presented, can be found
in Genesereth & Nilsson 1987. The paper ``Nonmonotonic
Reasoning in the Framework of the Situation Calculus'',
by Andrew Baker, found in the Brachman et al. volume, provides a quick but serviceable
introduction to the situation calculus at work. Another well-known approach in AI
to reasoning about time and change comes by way of James Allen's
``interval approach'' (1984).
Rina Dechter, Itay Meiri, and Judea Pearl's ``Temporal Constraint Networks'',
in Brachman et al. shows another (advanced) approach to time and action, one based
on networks; the authors compare their approach to Allen's.

When temporal logic is deployed to systematize
reasoning about the behavior of computer programs, it is often
recast as **dynamic logic**, wherein the operators we have identified are
associated with commands in a programming language. For a short but
elegant description of dynamic logic as reinterpretation of temporal logic,
see Thayse 1989 itself.

Mon Nov 17 14:57:06 EST 1997