 Given a set of atomic propositions \(PROP\), a temporal model for TL is a triple \(\mathcal{M}= \left\langle T, \prec, V \right\rangle\) where \(\mathcal{T} =\left\langle T, \prec \right\rangle\) is a temporal frame and \(V\) is a valuation assigning to each atomic proposition \(p\in{PROP}\) the set of time instants \(V(p) \subseteq T\) at which \(p\) is considered true. (Equivalently, the valuation can be given by a function \(I: T\times{PROP}\to \{\mathit{true},\mathit{false}\},\) which assigns a truth value to each atomic proposition at each time instant in the temporal frame, or by a labeling or state description \(L: T \to \mathcal{P}({PROP})\), which assigns to each time instant the set of atomic propositions that are considered true at that instant.)