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.

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:	Formal Methods and Tools (FMT)
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

Show download statistics for this publication

Repository Staff Only: item control page