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:
“Science is the language of the temporal world; love is that of the spiritual world. Man, indeed, describes more than he explains; while the angelic spirit sees and understands. Science saddens man; love enraptures the angel; science is still seeking, love has found. Man judges of nature in relation to itself; the angelic spirit judges of it in relation to heaven. In short to the spirits everything speaks.”
—Honoré De Balzac (1799–1850)