Linear temporal logic
= Linear temporal logic
{wiki}
= LTL
{c}
{synonym}
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\geq i$, and $G\alpha$ requires it at every $j\geq 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.