Model checking on state transition diagram

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. We present 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.