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:
“Listen to any musical phrase or rhythm, and grasp it as a whole, and you thereupon have present in you the image, so to speak, of the divine knowledge of the temporal order.”
—Josiah Royce (1855–1916)