Linear temporal logic

Summary

Linear temporal logic (LTL) is a modal logic whose formulas speak about a single infinite sequence of time steps. Besides the Boolean connectives it has the operators "next" ($X$) and "until" ($U$), and from them "eventually" ($F$) and "always" ($G$). It is a standard language for properties of reactive systems, such as "every request is eventually granted". It is a main input language of model checking.