 A formula \(\varphi\) of TL is valid in a temporal model \(\mathcal{M}\) (denoted \(\mathcal{M} \models \varphi\)) iff it is true at every time instant in that model. Moreover, we say that \(\varphi\) is valid in a temporal frame \(\mathcal{T}\) (denoted \(\mathcal{T} \models \varphi\)) iff it is valid in every model on that frame. Accordingly, a formula \(\varphi\) is valid (denoted \(\models \varphi\)) iff it is valid in all temporal frames, i.e. true at all time instants in all temporal models. A formula \(\varphi\) is satisfiable iff its negation is not valid, i.e. if \(\varphi\) is true at some time instant in some temporal model.