CTL May Be Ambiguous When Model Checking Moore Machines

  • Cédric Roux
  • Emmanuelle Encrenaz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2860)


The model checking problem is defined over Kripke structures. However, hardware designers often handle other models, such as Moore machines. When model checking their designs using CTL as a logic, they must translate them into Kripke structures. A given CTL property may be believed to be true (conversely false) over the Moore machine and in fact be false (conversely true) on the derived Kripke structure. This may lead to ambiguities if the designer does not fully understand the translation scheme he uses, which may be the case if he uses automatic tools. We present iCTL, a logic specifically designed to work with Moore machines, which extends CTL to help the designer removing possible ambiguities when model checking Moore machines. We show that it is strictly more expressive than CTL.


  1. 1.
    Brayton, R.K., Hachtel, G.D., Sangiovanni-Vincentelli, A., Somenzi, F., Aziz, A., Cheng, S.-T., Edwards, S., Khatri, S., Kukimoto, Y., Pardo, A., Qadeer, S., Ranjan, R.K., Sarwary, S., Shiple, T.R., Swamy, G., Villa, T.: VIS: a System for Verification and Synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 428–432. Springer, Heidelberg (1996)Google Scholar
  2. 2.
    Clarke, E.M., Allen Emerson, E., Prasad Sistla, A.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. on Programming Languages and Systems 8(2), 244–263 (1986)zbMATHCrossRefGoogle Scholar
  3. 3.
    Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional Model Checking. In: Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science, pp. 353–362 (1989)Google Scholar
  4. 4.
    Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science: Formal Models and Semantics, vol. B, ch. 16, pp. 995–1072. Elsevier, Amsterdam (1990)Google Scholar
  5. 5.
    McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Cédric Roux
    • 1
  • Emmanuelle Encrenaz
    • 1
  1. 1.ASIMUPMC – LIP6Paris CEDEX 5France

Personalised recommendations