 In linear, unbounded, forward-discrete temporal models \(\mathcal{M}= \left\langle T,\prec, V \right\rangle,\) where every instant \(t\) has a unique immediate successor \(s(t),\) it is natural to add a new temporal operator \(X\) (“NeXt Time” or “Tomorrow”) with  semantics:[2]