Source : Free On-Line Dictionary of Computing

temporal 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)