Volume 6: January - December 1996

Issue 4: August 1996


Buy one, get one free!!!

  • Buy one, get one free!!!
  • O. Kupferman and O. Grumberg Department of Computer Science, the Technion, Haifa 32000, Israel. Email: orna@cs.technion.ac.il


    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 lagged behind. However, users of these tools have to struggle with the limited expressive power of CTL and are often compelled to give up checking many important behaviours. 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, CTL2, 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 CTL2 and focus on the relation between CTL2 and CTL. We show that beyond the increase in the expressive power, a substantial advantage of CTL2 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 CTL2. Our model checker is of complexity linear in both the formula and the structure being checked, exactly as the one for CTL. In addition, we suggest an extension of it that, preserving its complexity, handles fairness.

    Keywords: Temporal logic, CTL, branching-time temporal logics, model checking

    Pages: 523 - 239

    Part of the OUP Journal of Logic and Computation WWW service

    General Information

    Click here to register with OUP.

    This page is maintained by OUP admin

    Last updated 09 Sep 96

    Part of the OUP Journals World Wide Web service.

    Copyright Oxford University Press, 1996