Linear temporal logic

A temporal logic interpreted along infinite paths in a transition system. At position $i$, $X\alpha$ requires $\alpha$ at $i+1$, $F\alpha$ requires it at some $j\ge i$, and $G\alpha$ requires it at every $j\ge i$. Strong until and weak until express conditions that hold up to a later event. A system satisfies a specification when all relevant initial paths in a transition system satisfy it.