Quantitative model checking of continuoustime Markov chains against timed automata specifications
Chen, Taolue and Han, Tingting and Katoen, JoostPieter and Mereacre, Alexandru (2009) Quantitative model checking of continuoustime Markov chains against timed automata specifications. In: 24th Annual IEEE Symposium on Logic In Computer Science, LICS 2009, 1114 Aug 2009, Los Angeles, USA (pp. pp. 309318).

PDF
362kB 
Abstract:  We study the following problem: given a continuoustime Markov chain (CTMC) C, and a linear realtime 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 singleclock 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