 That is, \(X\varphi\) is true at a time instant \(t\) iff \(\varphi\) is true at the immediate successor \(s(t)\) of \(t\). The Next Time operator was already mentioned by Prior (1967, Chapter IV.3), but its importance was first fully appreciated in the context of LTL.