Step Bounded Model Checker for Priced Timed Automata