The following technical report is available from http://aib.informatik.rwth-aachen.de:
Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre AIB 2009-02
We study the following problem: given a continuous-time Markov chain (CTMC) C, and a linear real-time property provided as a deterministic timed automaton (DTA) A, what is the probability of the set of paths of C that are accepted by A (C satisfies A)? It is shown that this set of paths is measurable and computing its probability can be reduced to computing the reachability probability in a piecewise deterministic Markov process (PDP). The reachability probability is characterized as the least solution of a system of integral equations and is shown to be approximated by solving a system of partial differential equations. For the special case of single-clock DTA, the system of integral equations can be transformed into a system of linear equations where the coefficients are solutions of ordinary differential equations.