\input zb-basic
\input zb-ioport
\iteman{io-port 05954738}
\itemau{Chen, Taolue; Han, Tingting; Katoen, Joost-Pieter; Mereacre, Alexandru}
\itemti{Observing continuous-time MDPs by 1-clock timed automata.}
\itemso{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).}
\itemab
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}$.
\itemrv{~}
\itemcc{}
\itemut{}
\itemli{doi:10.1007/978-3-642-24288-5\_2}
\end