Expressibility Results for Linear-time and Branching-time Logics

We investigate the expressive power of linear-time and branching-time temporal logics as fragments of the logic CTL*. We give a simple characterization of those CTL* formulas that can be expressed in linear-time logic. We also give a simple method for showing that certain CTL* formulas cannot be expressed in the branching-time logic CTL. Both results are illustrated with examples.