Which branching-time properties are effectively linear?

We characterize three successively more restrictive classes of `effectively linear' CTL{*} formulas, with and without fairness: the equi-linear formular:, which do not distinguish among models with the same language, the sub-linear formulas, which are preserved under model language inclusion and the strong linear formulas, which are characterized by a given omega -regular language. Moreover, strong linearity characterizes those CTL{*} formulas equivalent to LTL formulas. This taxonomy helps to clarify the expressive distinctions between CTL{*}, LTL and omega -regular languages. It has also practical implications. Verification tools based on language inclusion can handle any CTL{*} formula which is equi-linear; for purposes of model checking, and sub-linear for purposes of abstraction. Furthermore, minimization techniques that preserve the subset of CTL{*} which consists of only effectively linear formulas, result in smaller structures than bisimulation minimization.