PRISM
PRISM: Probabilistic symbolic model checker. In this paper we describe PRISM, a tool being developed at the University of Birmingham for the analysis of probabilistic systems. PRISM supports three probabilistic models: discrete-time Markov chains, Markov decision processes and continuous-time Markov chains. Analysis is performed through model checking such systems against specifications written in the probabilistic temporal logics PCTL and CSL. The tool features three model checking engines: one symbolic, using BDDs (binary decision diagrams) and MTBDDs (multi-terminal BDDs); one based on sparse matrices; and one which combines both symbolic and sparse matrix methods. PRISM has been successfully used to analyse probabilistic termination, performance, and quality of service properties for a range of systems, including randomized distributed algorithms, manufacturing systems and workstation clusters.
Keywords for this software
References in zbMATH (referenced in 254 articles , 2 standard articles )
Showing results 1 to 20 of 254.
Sorted by year (- Esmaeil Zadeh Soudjani, Sadegh; Abate, Alessandro; Majumdar, Rupak: Dynamic Bayesian networks for formal verification of structured stochastic processes (2017)
- Bortolussi, Luca; Milios, Dimitrios; Sanguinetti, Guido: Smoothed model checking for uncertain continuous-time Markov chains (2016)
- Cardelli, Luca; Tribastone, Mirco; Tschaikowski, Max; Vandin, Andrea: Symbolic computation of differential equivalences (2016)
- Chatterjee, Krishnendu; Chmelík, Martin; Gupta, Raghav; Kanodia, Ayush: Optimal cost almost-sure reachability in POMDPs (2016)
- Chatterjee, Krishnendu; Chmelík, Martin; Tracol, Mathieu: What is decidable about partially observable Markov decision processes with $\omega$-regular objectives (2016)
- Chen, Taolue; Primiero, Giuseppe; Raimondi, Franco; Rungta, Neha: A computationally grounded, weighted doxastic logic (2016)
- Ferrer Fioriti, Luis María; Hashemi, Vahid; Hermanns, Holger; Turrini, Andrea: Deciding probabilistic automata weak bisimulation: theory and practice (2016)
- Jegourel, Cyrille; Legay, Axel; Sedwards, Sean: Command-based importance sampling for statistical model checking (2016)
- Kirwan, Ryan; Miller, Alice; Porr, Bernd: Model checking learning agent systems using Promela with embedded C code and abstraction (2016)
- Kubota, Takahiro; Kakutani, Yoshihiko; Kato, Go; Kawano, Yasuhito; Sakurada, Hideki: Semi-automated verification of security proofs of quantum cryptographic protocols (2016)
- Lakin, Matthew R.; Stefanovic, Darko; Phillips, Andrew: Modular verification of chemical reaction network encodings via serializability analysis (2016)
- Olarte, C.; Chiarugi, D.; Falaschi, M.; Hermith, D.: A proof theoretic view of spatial and temporal dependencies in biochemical systems (2016)
- Petersen, Rasmus L.; Lakin, Matthew R.; Phillips, Andrew: A strand graph semantics for DNA-based computation (2016)
- Svoreňová, Mária; Kwiatkowska, Marta: Quantitative verification and strategy synthesis for stochastic games (2016)
- von Essen, Christian; Jobstmann, Barbara; Parker, David; Varshneya, Rahul: Synthesizing efficient systems in probabilistic environments (2016)
- Wijs, Anton; Katoen, Joost-Pieter; Bošnački, Dragan: Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components (2016)
- Xu, Ming; Zhang, Lijun; Jansen, David N.; Zhu, Huibiao; Yang, Zongyuan: Multiphase until formulas over Markov reward models: an algebraic approach (2016)
- Yang, Fan; Yang, Guowu; Hao, Yujie: The modeling library of eavesdropping methods in quantum cryptography protocols by model checking (2016)
- Zhang, Lijun; Jansen, David N.: A space-efficient simulation algorithm on probabilistic automata (2016)
- Abate, Alessandro; Soudjani, Sadegh Esmaeil Zadeh: Quantitative approximation of the probability distribution of a Markov process by formal abstractions (2015)
Further publications can be found at: http://www.prismmodelchecker.org/publications.php