Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications

Speaker

Alexandru Mereacre

Title Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
When 14.05.2008
Where Lecture Room Informatik 11
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)
Slides download