Notes:
The original publication is available at link.springer.com.

Abstract.
This paper considers the verification of continuoustime Markov decision process (CTMDPs) against singleclock deterministic timed automata (DTA) specifications. The central issue is to compute the maximum probability of the set of timed paths of a CTMDP C that are accepted by a DTA A. We show that this problem can be reduced to a linear programming problem whose coefficients are maximum timed reachability probabilities in a set of CTMDPs, which are obtained via a graph decomposition of the product of the CTMDP C and the region graph of the DTA A.
