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
= (S, R), where
S is an at-most-countable, non-empty set of states, and R is
a binary relation on S
satisfying a condition that makes it a functional relation, viz.,
(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,
, a counterpart to axiom K in
--do come out valid, formally speaking. Thayse 1989 and
Thayse 1991 also consider, in informative detail, how to go about proving
things in linear-time temporal logic (and in enhancements of it). We return
to some of the metatheory for this logic below.
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.