Model Matching for Finite State Machines