 The axiomatic system for LTL extends classical propositional logic by the K-axiom for \(G\), the K-axiom and the functionality axioms for \(X\), as well as by axioms providing fixed point characterizations of the reflexive versions of \(G\) and \(U\): 