Quantitative model checking of continuous-time Markov chains against timed automata specifications


Share/Save/Bookmark

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.

[img]
Preview
PDF
353Kb
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
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/68256
Official URL:http://dx.doi.org/10.1109/LICS.2009.21
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page