 The most popular and widely used temporal logic in computer science is the linear time temporal logic LTL, which was proposed in the seminal paper Pnueli (1977), and it was first explicitly axiomatized and studied in Gabbay et al. (1980). In LTL, time is conceived of as a linear, discrete succession of time instants, and the language involves the operators \(G,\) \(X\), and \(U\) (no past operators). LTL is interpreted over \(\left\langle \mathbf{N},\leq\right\rangle,\) where the temporal ordering is assumed to be reflexive as is common in computer science.