Exploiting functional dependencies in finite state machine verification

This paper proposes a novel verification method for finite state machines (FSMs), which automatically exploits the relation between the state encodings of the FSMs under consideration. It is based on the detection and utilization of functionally dependent state variables. This significantly extends the ability of the verification method to handle FSMs with similar state encodings. The effectiveness of the proposed method is illustrated by experimental results on well-known benchmarks