Approximate symbolic model checking of continous-time Markov chains


Share/Save/Bookmark

Baier, Christel and Katoen, Joost-Pieter and Hermanns, Holger (1999) Approximate symbolic model checking of continous-time Markov chains. In: 10th International Conference on Concurrency Theory, CONCUR '99, August 24-27, 1999, Eindhoven, The Netherlands (pp. pp. 146-162).

[img] PDF
Restricted to UT campus only
: Request a copy
332kB
Abstract:This paper presents a symbolic model checking algorithm for continuous-time Markov chains for an extension of the continuous stochastic logic CSL of Aziz et al. [1] The considered logic contains a time-bounded until-operator and a novel operator to express steady-state probabilities. We show that the model checking problem for this logic reduces to a system of linear equations (for unbounded until and the steady state-operator) and a Volterra integral equation system for time-bounded until. We propose a symbolic approximate method for solving the integrals using MTDDs (multi-terminal decision diagrams), a generalisation of MTBDDs. These new structures are suitable for numerical integration using quadrature formulas based on equally-spaced abscissas, like trapezoidal, Simpson and Romberg integration schemes.
Item Type:Conference or Workshop Item
Copyright:© 1999 Springer
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/63300
Official URL:http://dx.doi.org/10.1007/3-540-48320-9
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page