Abstract |
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 that C satisfies A? It is shown that this problem can be reduced to computing reachability probabilities in piecewise deterministic Markov processes (PDPs). These reachability probabilities are 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, it turns out that the system of integral equations can be transformed into a system of linear equations where the coefficients are solutions of ordinary differential equations (ODEs) |