Deterministic Timed Finite State Machines: Equivalence Checking and Expressive Power