  The satisfiability problem of the branching time logic CTL is studied in
terms of computational complexity. Tight upper and lower bounds are provided
for each temporal operator fragment. In parallel, the minimal model size is
studied with a suitable notion of minimality. Thirdly, flat CTL is
investigated, i.e., formulas with very low temporal operator nesting depth. A
sharp dichotomy is shown in terms of complexity and minimal models: Temporal
depth one has low expressive power, while temporal depth two is equivalent to
full CTL.
