Verification of Temporal Properties on Hybrid Automata by Simulation Relations