Sciweavers

PAPM
2001
Springer

Faster and Symbolic CTMC Model Checking

13 years 8 months ago
Faster and Symbolic CTMC Model Checking
Abstract. This paper reports on the implementation and the experiments with symbolic model checking of continuous-time Markov chains using multi-terminal binary decision diagrams (MTBDDs). Properties are expressed in Continuous Stochastic Logic (CSL) [7] which includes the means to express both transient and steady-state performance measures. We show that all CSL operators can be treated using standard operations on MTBDDs, thus allowing a rather straightforward implementation of symbolic CSL model checking on existing MTBDD-based platforms such as the verifier PRISM. The main result of the paper is an improvement of O(N) in the time complexity of checking time-bounded until-formulas, where N is the number of states in the CTMC under consideration. This result yields a drastic speed-up in the verification time of model checking CTMCs, both in the symbolic and non-symbolic case.
Joost-Pieter Katoen, Marta Z. Kwiatkowska, Gethin
Added 30 Jul 2010
Updated 30 Jul 2010
Type Conference
Year 2001
Where PAPM
Authors Joost-Pieter Katoen, Marta Z. Kwiatkowska, Gethin Norman, David Parker
Comments (0)