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 283 articles , 2 standard articles )

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

1 2 3 ... 13 14 15 next

  1. Bortolussi, Luca; Milios, Dimitrios; Sanguinetti, Guido: Smoothed model checking for uncertain continuous-time Markov chains (2016)
  2. Chatterjee, Krishnendu; Chmelík, Martin; Gupta, Raghav; Kanodia, Ayush: Optimal cost almost-sure reachability in POMDPs (2016)
  3. Chatterjee, Krishnendu; Chmelík, Martin; Tracol, Mathieu: What is decidable about partially observable Markov decision processes with $\omega$-regular objectives (2016)
  4. Chen, Taolue; Primiero, Giuseppe; Raimondi, Franco; Rungta, Neha: A computationally grounded, weighted doxastic logic (2016)
  5. Ferrer Fioriti, Luis María; Hashemi, Vahid; Hermanns, Holger; Turrini, Andrea: Deciding probabilistic automata weak bisimulation: theory and practice (2016)
  6. Kubota, Takahiro; Kakutani, Yoshihiko; Kato, Go; Kawano, Yasuhito; Sakurada, Hideki: Semi-automated verification of security proofs of quantum cryptographic protocols (2016)
  7. Lakin, Matthew R.; Stefanovic, Darko; Phillips, Andrew: Modular verification of chemical reaction network encodings via serializability analysis (2016)
  8. Olarte, C.; Chiarugi, D.; Falaschi, M.; Hermith, D.: A proof theoretic view of spatial and temporal dependencies in biochemical systems (2016)
  9. Petersen, Rasmus L.; Lakin, Matthew R.; Phillips, Andrew: A strand graph semantics for DNA-based computation (2016)
  10. von Essen, Christian; Jobstmann, Barbara; Parker, David; Varshneya, Rahul: Synthesizing efficient systems in probabilistic environments (2016)
  11. Xu, Ming; Zhang, Lijun; Jansen, David N.; Zhu, Huibiao; Yang, Zongyuan: Multiphase until formulas over Markov reward models: an algebraic approach (2016)
  12. Zhang, Lijun; Jansen, David N.: A space-efficient simulation algorithm on probabilistic automata (2016)
  13. Abate, Alessandro; Soudjani, Sadegh Esmaeil Zadeh: Quantitative approximation of the probability distribution of a Markov process by formal abstractions (2015)
  14. 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)
  15. Ballarini, Paolo; Duflot, Marie: Applications of an expressive statistical model checking approach to the analysis of genetic circuits (2015)
  16. Barbot, Beno^ıt; Kwiatkowska, Marta: On quantitative modelling and verification of DNA walker circuits using stochastic Petri nets (2015)
  17. Barbuti, Roberto; Bove, Pasquale; Milazzo, Paolo; Pardini, Giovanni: Minimal probabilistic P systems for modelling ecological systems (2015)
  18. Barnat, Jiří: Quo vadis explicit-state model checking (2015)
  19. Bartocci, Ezio; Bortolussi, Luca; Nenzi, Laura; Sanguinetti, Guido: System design of stochastic models using robustness of temporal properties (2015)
  20. Boreale, Michele: Analysis of probabilistic systems via generating functions and Padé approximation (2015)

1 2 3 ... 13 14 15 next

Further publications can be found at: