Verifying Soft Deadlines with Probabilistic Timed Automata