Model Checking Continuous-Time Markov Chains Against Timed Automata Specifications

by Alexandru Mereacre and Joost-Pieter Katoen

Abstract
This talk will explain how to verify a continuous-time Markov chain (CTMC) C against a linear real-time specification given as a deterministic timed automaton (DTA) A with finite or Muller acceptance conditions. A CTMC is a simple probabilistic hybrid system where the flow is a linear function and the waiting time in every state of the CTMC is governed by an exponential distribution. The verification of CTMCs is done by taking the product between the CTMC and DTA. This result into a determinstic Markovian timed automata which are basically CTMC with time constraints. In terms of probabilistic hybrid systems this is equivalent to having state invariants.

It will be shown that under finite acceptance criteria this equals the reachability probability in a piecewise deterministic Markov process (PDP), whereas for Muller acceptance criteria it coincides with the reachability probability of terminal strongly connected components in such PDP.  Reachability probabilities in our PDPs are then characterized as the least solution of a system of Volterra integral equations of the second type and are shown to be approximated by the solution of a system of partial differential equations.
For the special case of single-clock DTA, this integral equation system can be transformed into a system of linear equations where the coefficients are solutions of ordinary differential equations.

Reference

Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre:

Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications. LICS 2009, 309-318