Model checking on state transition diagram

ABSTRACT

Computation Tree Logic (CTL) model checking is sensitive to state explosion. Conventionally, CTL semantics is defined over Kripke structure where each state is labelled with all the atomic propositions. For open systems, this necessitates input labeling of the states. In contrast, the common model, which is used for sequential circuit design, is the finite state machine (FSM) model, or equivalently, the state transition diagram (STD), where the inputs are associated not with the states but with the transitions. Thus, to use a conventional CTL model checker, the STD has to be converted first to the Kripke structure and then applying the model checking algorithm on the Kripke structure. The need for associating input labels to the states results in state explosion which finally tells upon the model checking efficiency. The paper presents the CTL semantics over STD structures and develops a model checking algorithm which works directly over the STD. A performance gain over conventional model checking by an exponential factor results in the process, especially for open systems.

REFERENCES

• 1: M C Browne , E M Clarke , D L Dill , B Mishra, Automatic verification of sequential circuits using temporal logic, IEEE Transactions on Computers, v.35 n.12, p.1035-1044, Dec. 1986 [doi>10.1109/TC.1986.1676711]
• 2: E. Clarke, O. Grumberg, and D. Peled, Model Checking. MIT Press, 2000.
• 3: Z. Kohavi, Switching and Automata Theory. Tata-McGraw Hill, Pub. Co. Ltd., New Delhi, 1978.
• 4: M. Y. Vardi, On the complexity of modular model checking, Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, p.101, June 26-29, 1995
• 5: Moshe Y. Vardi, Verification of Open Systems, Proceedings of the 17th Conference on Foundations of Software Technology and Theoretical Computer Science, p.250-266, December 18-20, 1997
• 6: Orna Kupferman , Moshe Y. Vardi, Module Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.75-86, August 03, 1996
• 7: Orna Kupferman , Moshe Y. Vardi, Model Checking Revisited, Proceedings of the 9th International Conference on Computer Aided Verification, p.36-47, June 22-25, 1997
• 8: Pallab Dasgupta , Arindam Chakrabarti , P. P. Chakrabarti, Open Computation Tree Logic for Formal Verification of Modules, Proceedings of the 2002 conference on Asia South Pacific design automation/VLSI Design, p.735, January 07-11, 2002
• 9: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 10: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 11: J. Burch, E. Clarke, K. McMillian, D. Dill, and L. Hawang, "Symbolic Model Checking for Sequential Circuit Verification," IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst, vol. 13(4), pp. 401--424, 1994.

INDEX TERMS

Keywords:
CTL model checking, Finite State Machine (FSM), Kripke structure, State Transition Diagram (STD)