Approximate Symbolic Model Checking of Continuous-Time Markov Chains

Christel BaierChristel Baier, Joost-Pieter KatoenJoost-Pieter Katoen, Holger HermannsHolger Hermanns

DOI Link

Christel Baier, Joost-Pieter Katoen, Holger Hermanns
Approximate Symbolic Model Checking of Continuous-Time Markov Chains
10th International Conference on Concurrency Theory (CONCUR), volume 1664 of Lecture Notes in Computer Science, 146--161, 1999. Springer

Details
Bibtex

KurzfassungAbstract
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 steadystate 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 timebounded 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.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/3-540-48320-9_12.

@inproceedings{BKH1999,
  author    = {Christel Baier and Joost-Pieter Katoen and Holger Hermanns},
  title     = {Approximate Symbolic Model Checking of Continuous-Time Markov
               Chains},
  booktitle = {10th International Conference on Concurrency Theory (CONCUR)},
  series    = {Lecture Notes in Computer Science},
  volume    = {1664},
  publisher = {Springer},
  year      = {1999},
  pages     = {146--161},
  doi       = {10.1007/3-540-48320-9_12}
}