Approximate Symbolic Model Checking of Continuous-Time Markov Chains

d abstract) Christel Baiera, Joost-Pieter Katoenb;c and Holger Hermannsc aLehrstuhl fur Praktische Informatik II, University of Mannheim 68131 Mannheim, Germany bLehrstuhl fur Informatik 7, University of Erlangen-Nurnberg Martensstra e 3, 91058 Erlangen, Germany cSystems Validation Centre, University of Twente P.O. Box 217, 7500 AE Enschede, The Netherlands 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. Thes...

• Type: Conference
• Year: 1999
• Where: CONCUR
• Authors: Christel Baier, Joost-Pieter Katoen, Holger Hermanns
• Keywords: Blehrstuhl Fur Informatik, CONCUR 1999, Distributed And Parallel Computing, Fur Praktische Informatik, Model Checking