 A temporal formula of TL expresses (defines or corresponds to) a property of temporal frames if the formula is valid in all and only those frames that have the property. The most important correspondences between properties of temporal frames (see list in  Section 2.1)  and TL formulae include: 