AIB 2009-02: Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications

[Carsten Fuhs]

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.