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.

References in zbMATH (referenced in 251 articles , 2 standard articles )

Showing results 1 to 20 of 251.
Sorted by year (citations)

1 2 3 ... 11 12 13 next

  1. Bortolussi, Luca; Milios, Dimitrios; Sanguinetti, Guido: Smoothed model checking for uncertain continuous-time Markov chains (2016)
  2. Cardelli, Luca; Tribastone, Mirco; Tschaikowski, Max; Vandin, Andrea: Symbolic computation of differential equivalences (2016)
  3. Chatterjee, Krishnendu; Chmelík, Martin; Gupta, Raghav; Kanodia, Ayush: Optimal cost almost-sure reachability in POMDPs (2016)
  4. Chatterjee, Krishnendu; Chmelík, Martin; Tracol, Mathieu: What is decidable about partially observable Markov decision processes with $\omega$-regular objectives (2016)
  5. Chen, Taolue; Primiero, Giuseppe; Raimondi, Franco; Rungta, Neha: A computationally grounded, weighted doxastic logic (2016)
  6. Ferrer Fioriti, Luis María; Hashemi, Vahid; Hermanns, Holger; Turrini, Andrea: Deciding probabilistic automata weak bisimulation: theory and practice (2016)
  7. Jegourel, Cyrille; Legay, Axel; Sedwards, Sean: Command-based importance sampling for statistical model checking (2016)
  8. Kirwan, Ryan; Miller, Alice; Porr, Bernd: Model checking learning agent systems using Promela with embedded C code and abstraction (2016)
  9. Kubota, Takahiro; Kakutani, Yoshihiko; Kato, Go; Kawano, Yasuhito; Sakurada, Hideki: Semi-automated verification of security proofs of quantum cryptographic protocols (2016)
  10. Lakin, Matthew R.; Stefanovic, Darko; Phillips, Andrew: Modular verification of chemical reaction network encodings via serializability analysis (2016)
  11. Olarte, C.; Chiarugi, D.; Falaschi, M.; Hermith, D.: A proof theoretic view of spatial and temporal dependencies in biochemical systems (2016)
  12. Petersen, Rasmus L.; Lakin, Matthew R.; Phillips, Andrew: A strand graph semantics for DNA-based computation (2016)
  13. Svoreňová, Mária; Kwiatkowska, Marta: Quantitative verification and strategy synthesis for stochastic games (2016)
  14. von Essen, Christian; Jobstmann, Barbara; Parker, David; Varshneya, Rahul: Synthesizing efficient systems in probabilistic environments (2016)
  15. Xu, Ming; Zhang, Lijun; Jansen, David N.; Zhu, Huibiao; Yang, Zongyuan: Multiphase until formulas over Markov reward models: an algebraic approach (2016)
  16. Zhang, Lijun; Jansen, David N.: A space-efficient simulation algorithm on probabilistic automata (2016)
  17. Abate, Alessandro; Soudjani, Sadegh Esmaeil Zadeh: Quantitative approximation of the probability distribution of a Markov process by formal abstractions (2015)
  18. Baier, Christel; Daum, Marcus; Engel, Benjamin; Härtig, Hermann; Klein, Joachim; Klüppelholz, Sascha; Märcker, Steffen; Tews, Hendrik; Völp, Marcus: Locks: picking key methods for a scalable quantitative analysis (2015)
  19. Ballarini, Paolo; Duflot, Marie: Applications of an expressive statistical model checking approach to the analysis of genetic circuits (2015)
  20. Barbot, Beno^ıt; Kwiatkowska, Marta: On quantitative modelling and verification of DNA walker circuits using stochastic Petri nets (2015)

1 2 3 ... 11 12 13 next

Further publications can be found at: