 A model \(\sM\) for propositional temporal logic consists of a nonempty set \(T\) of moments of time, an earlier than relation \(\prec\) and a valuation function \(I\) which for each moment of time and each proposition letter \(q\) assigns a truth value \(I_{\sM ,t}(q)\). The following definition characterizes \(I_{\sM ,t}(\phi)\) for the temporal operators. 