Exploiting functional dependencies in finite state machineverification

摘要

This paper proposes a novel verification method for finite statemachines (FSMs), which automatically exploits the relation between thestate encodings of the FSMs under consideration. It is based on thedetection and utilization of functionally dependent state variables.This significantly extends the ability of the verification method tohandle FSMs with similar state encodings. The effectiveness of theproposed method is illustrated by experimental results on well-knownbenchmarks