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".

(1997-01-21)