Counterexample for Timed Probabilistic Reachability in Uniform CTMDP

A uniform continuous-time Markov decision process (CTMDP) is a CTMDP where the exit rate from every state is the same for all states. This paper solves the problem of generating counterexamples for timed probabilistic reachability in uniform CTMDP. The key contribution is an efficient algorithm for computing a minimal part of a uniform CTMDP that indicates the violation of time-bounded reachability probabilities.