A logic-based approach for the verification of UML timed models