C. Baier, J.-P. Katoen, and H. Hermanns.
Approximate symbolic model checking of continous-time Markov chains.
In J.C.M. Baeten and S. Mauw (eds), Concurrency Theory (CONCUR'99), LNCS 
1664, pages 146-162, Eindhoven, The Netherlands, 1999.  Springer-Verlag.

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.  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.