About

Linear temporal logic (also called linear-time temporarl logic), usually called LTL, is a temporal logic that can encode assertions about the future of traces a linear model of time. In addition to the propositional calculus ($\phi \wedge \psi$, $\phi \vee \psi$, $\neg \phi$), LTL includes the following operators:

• $\mathop{\mathbf{X}} \phi$ (sometimes written $\mathbf{N}\,\phi$) “next $\phi$”: $\phi$ will be true in the next step;
• $\mathop{\mathbf{G}} \phi$ “globally $\phi$”: $\phi$ will be true in every step;
• $\mathop{\mathbf{F}} \phi$ “finally $\phi$”: $\phi$ will be true at some step eventually;
• $\phi \mathop{\mathbf{U}} \psi$ “$\phi$ until $\psi$”: $\phi$ will remain true until some step when $\psi$ becomes true (possibly excluding that step), and this will happen eventually;
• $\phi \mathop{\mathbf{W}} \psi$ “$\phi$ weakly until $\psi$”: $\phi$ will remain true until some step when $\psi$ becomes true, or $\phi$ will remain true forever;
• $\phi \mathop{\mathbf{R}} \psi$ “$\phi$ release $\psi$”: $\phi$ will remain true until some step when $\psi$ becomes true (including that step), or $\phi$ will remain true forever.