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:
“When once a certain class of people has been placed by the temporal and spiritual authorities outside the ranks of those whose life has value, then nothing comes more naturally to men than murder.”
—Simone Weil (1909–1943)