Temporal logic

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