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.
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.
|xUy||Until: x holds until y doesn't anymore (and may hold after)|
|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|