 A complete axiomatization of CTL can be obtained by replacing the axioms of LTL by their path-quantified versions. For proofs of completeness, see Emerson (1990) and Goldblatt (1992). For CTL* more axioms must be added to account for the combinations of temporal and modal operators and to enforce the limit closure property of trees. A complete axiomatization for CTL* was obtained by Reynolds (2001), and a completeness result for the extension of CTL* with past operators is established in Reynolds (2005). A sketch of the axiomatic system for CTL can be found in the supplementary document: