Temporal Operators
Temporal logic has two kinds of operators: logical operators and modal operators . Logical operators are usual truth-functional operators . The modal operators used in Linear Temporal Logic and Computation Tree Logic are defined as follows.
| Textual | Symbolic | Definition | Explanation | Diagram |
|---|---|---|---|---|
| Binary operators | ||||
| U | Until: holds at the current or a future position, and has to hold until that position. At that position does not have to hold any more. | |||
| R | Release: releases if is true until the first position in which is true (or forever if such a position does not exist). | |||
| Unary operators | ||||
| N | Next: has to hold at the next state. (X is used synonymously.) | |||
| F | Future: eventually has to hold (somewhere on the subsequent path). | |||
| G | Globally: has to hold on the entire subsequent path. | |||
| A | All: has to hold on all paths starting from the current state. | |||
| E | Exists: there exists at least one path starting from the current state where holds. | |||
Alternate symbols:
- operator R is sometimes denoted by V
- The operator W is the weak until operator: is equivalent to
Unary operators are well-formed formulas whenever B is well-formed. Binary operators are well-formed formulas whenever B and C are well-formed.
In some logics, some operators cannot be expressed. For example, N operator cannot be expressed in Temporal Logic of Actions.
Read more about this topic: Temporal Logic
Famous quotes containing the word temporal:
“Social questions are too sectional, too topical, too temporal to move a man to the mighty effort which is needed to produce great poetry. Prison reform may nerve Charles Reade to produce an effective and businesslike prose melodrama; but it could never produce Hamlet, Faust, or Peer Gynt.”
—George Bernard Shaw (1856–1950)