HomeNewsCase StudiesPeoplePublications
[CHKM11a] T. Chen, T. Han, J.-P. Katoen, A. Mereacre. Observing Continuous-Time MDPs by 1-Clock Timed Automata. In Proc. 5th Interntaional Workshop on Reachability Problems (RP'11), volume 6945 of LNCS, pages 2-25, Springer. September 2011. [pdf] [bib]
Downloads:  pdf pdf (394 KB)  bib bib
Notes: The original publication is available at www.springerlink.com.
Abstract. This paper considers the verification of continuous-time Markov decision process (CTMDPs) against single-clock 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.