temporal logic
<logic> An extension of predicate calculus which includes notation for
arguing about *when* statements are true. Time is discrete and extends
indefinitely into the future. Three prefix operators, represented by a circle,
square and diamond mean "is true at the next time instant", "is true from now
on" and "is eventually true". x U y means x is true until y is true. x P y means
x precedes y.
There are two types of formula: "state formulae" about things true at one point
in time, and "path formulae" about things true for a sequence of steps. An
example of a path formula is "x U y", and example of a state formula is "next x"
or a simple atomic formula such at "waiting".
"true until" in this context means that a state formula holds at every point in
time up to a point when another formula holds. "x U y" is the "strong until" and
implies that there is a time when y is true. "x W y" is the "weak until" in
which it is not necessary that y holds eventually.
There are two types of temporal logic used: branching time and linear time. The
basic propositional temporal logic cannot differentiate between the two, though.
Linear time considers only one possible future, in branching time you have
several alternative futures. In branching temporal logic you have the extra
operators "A" (for "all futures") and "E" (for "some future"). For example,
"A(work U go_home)" means "I will work until I go home" and "E(work U go_home)"
means "I may work until I go home".
(19970121)
Nearby terms:
TEMPO « Tempo « temporal database « temporal
logic » Tempura » Ten15 » tendinitis
