Quantitative model checking of continuous-time Markov chains against timed automata specifications
Chen, Taolue and Han, Tingting and Katoen, Joost-Pieter and Mereacre, Alexandru (2009) Quantitative model checking of continuous-time Markov chains against timed automata specifications. In: 24th Annual IEEE Symposium on Logic In Computer Science, LICS 2009, 11-14 Aug 2009, Los Angeles, USA (pp. pp. 309-318).
|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 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.
|Item Type:||Conference or Workshop Item|
|Copyright:||© 2009 IEEE|
Electrical Engineering, Mathematics and Computer Science (EEMCS)
|Link to this item:||http://purl.utwente.nl/publications/68256|
|Export this item as:||BibTeX|
Daily downloads in the past month
Monthly downloads in the past 12 months
Repository Staff Only: item control page