An efficient verifier for finite state machines

The correctness-checking problem of a finite-state machine is considered. The concept of machine cover is revived and used as the basis of the formulation of the verification problem of the design correctness of finite-state machines. The concept of machine cover enables the verifier to efficiently check the sufficiency. The verifier checks to see if the implementation is correct with respect to its specification, which is given as a form of finite-state machine. Since in general the state encoding information is not available for verification purposes, it is assumed that the encoding information is missing. An efficient algorithm for the verification problem is presented along with its implementation. Experimental results show that the approach is promising in terms of speed