Temporal logic

From Esolang
Jump to: navigation, search

Temporal logic is a system of logic that deals with logic as a function of time. Variables can be true sometimes but not always, and you can define when this happens, and you can tell it whether or not to do so, et cetera.

Paths

Temporal logic can be either linear or branching. In linear temporal logic, the state of the program is a definite timeline. In branching temporal logic, on the other hand, state follows a tree.

Operators

Operator Meaning
xUy Until: x holds until y doesn't anymore (and may hold after)
xRy Release: ???
Nx Next: x must hold at the next state
Fx Future: x must hold sometime in the future
Gx Global: x must hold for the entirety of the subsequent path (like future, but forever)
Ax All: Behaves like Global for ALL paths (x must hold on all paths from the current state).
Ex Exists: x holds on at least one path from the current state