Quantitative Model Checking of Continuous-Time Markov Chains Against
Timed Automata Specifications
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre
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.