Performance Analysis of Probabilistic Timed Automata using Digital Clocks