CTL May Be Ambiguous When Model Checking Moore Machines
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.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
- 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.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