temporal logic


temporal logic

(logic)An extension of predicate calculus which includesnotation for arguing about *when* statements are true. Timeis discrete and extends indefinitely into the future. Threeprefix operators, represented by a circle, square and diamondmean "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 istrue. x P y means x precedes y.

There are two types of formula: "state formulae" about thingstrue at one point in time, and "path formulae" about thingstrue 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 asimple atomic formula such at "waiting".

"true until" in this context means that a state formula holdsat every point in time up to a point when another formulaholds. "x U y" is the "strong until" and implies that thereis a time when y is true. "x W y" is the "weak until" inwhich it is not necessary that y holds eventually.

There are two types of temporal logic used: branching time andlinear time. The basic propositional temporal logic cannotdifferentiate between the two, though. Linear time considersonly one possible future, in branching time you have severalalternative futures. In branching temporal logic you have theextra operators "A" (for "all futures") and "E" (for "somefuture"). For example, "A(work U go_home)" means "I will workuntil I go home" and "E(work U go_home)" means "I may workuntil I go home".