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:
“What’s this, Aurora Leigh,
You write so of the poets and not laugh?
Those virtuous liars, dreamers after dark,
Exaggerators of the sun and moon,
And soothsayers in a tea-cup? I write so
Of the only truth-tellers, now left to God,—
The only speakers of essential truth,
Opposed to relative, comparative,
And temporal truths;...
The only teachers who instruct mankind,
From just a shadow on a charnel-wall.”
—Elizabeth Barrett Browning (1806–1861)