Loading...
Please wait, while we are loading the content...
Similar Documents
Probabilistic symbolic model checking with PRISM: A hybrid approach (2002)
| Content Provider | CiteSeerX |
|---|---|
| Author | Parker, David Kwiatkowska, Marta Norman, Gethin |
| Abstract | Abstract. In this paper we introduce PRISM, a probabilistic model checker, and describe the efficient symbolic techniques we have developed during its implementation. PRISM is a tool for analysing probabilistic systems. It supports three models: discrete-time Markov chains, continuous-time Markov chains and Markov decision processes. Analysis is performed through model checking specifications in the probabilistic temporal logics PCTL and CSL. Motivated by the success of model checkers such as SMV, which use BDDs (binary decision diagrams), we have developed an implementation of PCTL and CSL model checking based on MTBDDs (multi-terminal BDDs) and BDDs. Existing work in this direction has been hindered by the generally poor performance of MTBDD-based numerical computation, which is often substantially slower than explicit methods using sparse matrices. We present a novel hybrid technique which combines aspects of symbolic and explicit approaches to overcome these performance problems. For typical examples, we achieve orders of magnitude speed-up compared to MTBDDs and are able to almost match the speed of sparse matrices whilst maintaining considerable space savings. 1 |
| File Format | |
| Journal | International Journal on Software Tools for Technology Transfer (STTT |
| Publisher Date | 2002-01-01 |
| Access Restriction | Open |
| Subject Keyword | Novel Hybrid Technique Mtbdd-based Numerical Computation Binary Decision Diagram Efficient Symbolic Technique Probabilistic Model Checker Model Checker Performance Problem Continuous-time Markov Chain Markov Decision Probabilistic System Poor Performance Typical Example Discrete-time Markov Chain Hybrid Approach Csl Model Multi-terminal Bdds Considerable Space Saving Explicit Approach Probabilistic Symbolic Model Sparse Matrix Probabilistic Temporal Logic Pctl |
| Content Type | Text |
