Model Reduction of Finite State Machines by Contraction