Buy One, Get One Free !!!
-------------------------

The exponential gap between CTL and LTL model-checking complexity,
led to a development of model-checking tools for CTL, while model
checkers for LTL have stayed behind. However, users of those tools
have to struggle with the limited expressive power of CTL and are
often compelled to give up checking many important behaviors. As a
matter of course, finding specification languages which are strictly
more expressive than CTL and yet maintain its attractive
model-checking complexity, is a challenging problem and has been an
active area of research. In this paper we introduce such a language. 

Our language, CTL^2, is an outcome of a new approach for defining
sub-languages of CTL*. The approach allows a bounded number of
linear-time operators within the path formulas of CTL*.
We discuss the expressive power of CTL^2 and, in particular, focus
on the relation between CTL^2 and CTL. We show that beyond the
increase in the expressive power, a substantial advantage of CTL^2 is
the neat and intuitive presentation it provides for specifications
whose CTL equivalences are complicated and very hard to understand. We
introduce a model-checking procedure for CTL^2. Our model checker is
of complexity linear in both the formula and the structure being
checked, just as the one for CTL. In addition, we suggest an extension
of it that, preserving its complexity, handles fairness.