Model checking has been popular and successfully used in industry. A restriction of the model checking paradigm comes from the fact that the results of verification depend on the accuracy of the model which has been constructed for analysis. Since verification techniques have become more efficient and more prevalent, many people  have sought to extend the range of models and specification formalisms to whichmodel checking can be applied. A good example is the field of probabilistic model checking. Indeed the behaviour of many real-life processes is inherently stochastic. Therefore, different formalisms in which the underlying system has been modelled by Markovian models has been proposed. CSL for Continuous Time Markov Chains(CTMC) [1], PCTL for Discrete Time Markov Chains (PCTL) [10] and Markov Decision Processes [5]. Furthermore these formalisms are extended with cost and reward models. Indeed, formal verification using model checking and performance and dependability evaluation have a lot of things in common. Markovian models have been largely used in performance, dependability, availability and reliability analysis of computer and communication systems. In order to specify the models of real systems which become more and more large and sophisticated, high-level specification techniques as stochastic Petri nets, stochastic process algebra, stochastic automata networks, etc. have been proposed. Therefore it is possible to construct very large and complex models by using a high-level specification technique. Once the model is constructed, it is analyzed to evaluate the performability, availability measures which are defined by steady-state or transient-state probabilities. The possibility to express complex measures of interest can be provided by formalisms which are extension of formal logics: Branching-time logics as Computational Tree Logic (CTL) let us to express state-based properties and properties over paths [10], Continuous Stochastic Logic (CSL) [1] which allows to specify probabilistic measures over paths for CTMCs as well as standard transient-state and steady-state measures in a compact and unambiguous way.

Stochastic model checking can be performed by numerical or statistical methods. In [19, 17], authors propose a statistical approach based on Monte Carlo simulation and statistical hypothesis testing for CSL model checking. To perform model checking by numerical analysis we need to compute transient-state or steady-state distribution of the underlying Markov chains. The numerical model checking has been studied extensively and numerous algorithms have been devised. These have been implemented in different model checkers. It is well-known that despite the considerable works in the domain, the numerical Markovian analysis still remains a problem. This problem known as the state space explosion : the state space size increases exponentially with parameter sizes of the model. Many of works have been done and are under study to overcome this problem by applyingmodel driven methods as decomposition, bounding methods, matrix geometric, stockage techniques, etc.

The reason that non-probabilistic model checking has been so successful in the real worlds is that an important amount of work has been done to develop efficient implementation techniques for it. One of the most successful approaches is symbolic model checking. For instance, Binary Decision Diagrams (BDD) are a data structure exploiting the regularity of model description via high level formalism leading in an compact representation of large models. Efficient manipulation algorithms have been developed under this data structure and its extension multi-terminal binary decision diagrams (MTBDD).