05954738

a

05954738 Chen, Taolue Han, Tingting Katoen, Joost-Pieter Mereacre, Alexandru Observing continuous-time MDPs by 1-clock timed automata. Delzanno, Giorgio (ed.) et al., Reachability problems. 5th international workshop, RP 2011, Genoa, Italy, September 28--30, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-24287-8/pbk). Lecture Notes in Computer Science 6945, 2-25 (2011). 2011 Berlin: Springer EN

doi:10.1007/978-3-642-24288-5_2

Summary: This paper considers the verification of continuous-time Markov decision process (CTMDP s) 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 $\mathcal{C}$ that are accepted by a DTA $\mathcal{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 $\mathcal{C}$ and the region graph of the DTA $\mathcal{A}$.