CTL reachability and safety operators are least and greatest fixed points of monotone predicate transformers on the complete powerset lattice. Symbolic model checking evaluates these fixpoints in polynomial rounds via BDDs.