 The logic CTL became widely used owing to its good computational properties with regard to model checking, having linear complexity both in the size of the input formula and in the size of the input model (as finite transition system). However, CTL is not very expressive, which led to its extension CTL*. The logic CTL* is expressively much more powerful and subsumes the linear time temporal logic LTL, but it has higher complexities of model checking (PSPACE) and of deciding satisfiability (2EXPTIME). For references and further details, see Emerson (1990) and Stirling (1992).