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.

• Type: Conference
• Year: 2001
• Where: PAPM
• Authors: Joost-Pieter Katoen, Marta Z. Kwiatkowska, Gethin Norman, David Parker
• Keywords: Mathematics, Model Checking, PAPM 2001, Symbolic Csl Model, Symbolic Model Checking