 Branching time logics are extensively used in computer science. The most popular ones are the computation tree logics CTL and CTL*, which are variations of the Peircean and Ockhamist branching time temporal logics. They are interpreted on the class of so-called computation trees, where every history has the order type of the natural numbers. These trees are naturally obtained as tree unfoldings of discrete transition systems and represent the possible infinite computations arising in such systems. While CTL historically preceded CTL*, nowadays CTL is often viewed as a fragment of CTL*, and we follow this convention here. 