A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking