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.


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

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

1 2 3 ... 12 13 14 next

  1. Chatterjee, Krishnendu; Křetínská, Zuzana; Křetínský, Jan: Unifying two views on multiple mean-payoff objectives in Markov decision processes (2017)
  2. Esmaeil Zadeh Soudjani, Sadegh; Abate, Alessandro; Majumdar, Rupak: Dynamic Bayesian networks for formal verification of structured stochastic processes (2017)
  3. Bortolussi, Luca; Milios, Dimitrios; Sanguinetti, Guido: Smoothed model checking for uncertain continuous-time Markov chains (2016)
  4. Cardelli, Luca; Kwiatkowska, Marta; Whitby, Max: Chemical reaction network designs for asynchronous logic circuits (2016)
  5. Cardelli, Luca; Tribastone, Mirco; Tschaikowski, Max; Vandin, Andrea: Symbolic computation of differential equivalences (2016)
  6. Chatterjee, Krishnendu; Chmelík, Martin; Gupta, Raghav; Kanodia, Ayush: Optimal cost almost-sure reachability in POMDPs (2016)
  7. Chatterjee, Krishnendu; Chmelík, Martin; Tracol, Mathieu: What is decidable about partially observable Markov decision processes with $\omega$-regular objectives (2016)
  8. Chen, Taolue; Primiero, Giuseppe; Raimondi, Franco; Rungta, Neha: A computationally grounded, weighted doxastic logic (2016)
  9. Esparza, Javier; Křetínský, Jan; Sickert, Salomon: From LTL to deterministic automata. A safraless compositional approach (2016)
  10. Ferrer Fioriti, Luis María; Hashemi, Vahid; Hermanns, Holger; Turrini, Andrea: Deciding probabilistic automata weak bisimulation: theory and practice (2016)
  11. Jegourel, Cyrille; Legay, Axel; Sedwards, Sean: Command-based importance sampling for statistical model checking (2016)
  12. Kamaleson, Nishanthan; Parker, David; Rowe, Jonathan E.: Finite-horizon bisimulation minimisation for probabilistic systems (2016)
  13. Kirwan, Ryan; Miller, Alice; Porr, Bernd: Model checking learning agent systems using Promela with embedded C code and abstraction (2016)
  14. Kubota, Takahiro; Kakutani, Yoshihiko; Kato, Go; Kawano, Yasuhito; Sakurada, Hideki: Semi-automated verification of security proofs of quantum cryptographic protocols (2016)
  15. Lakin, Matthew R.; Stefanovic, Darko; Phillips, Andrew: Modular verification of chemical reaction network encodings via serializability analysis (2016)
  16. Olarte, C.; Chiarugi, D.; Falaschi, M.; Hermith, D.: A proof theoretic view of spatial and temporal dependencies in biochemical systems (2016)
  17. Petersen, Rasmus L.; Lakin, Matthew R.; Phillips, Andrew: A strand graph semantics for DNA-based computation (2016)
  18. Svoreňová, Mária; Kwiatkowska, Marta: Quantitative verification and strategy synthesis for stochastic games (2016)
  19. von Essen, Christian; Jobstmann, Barbara; Parker, David; Varshneya, Rahul: Synthesizing efficient systems in probabilistic environments (2016)
  20. 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)

1 2 3 ... 12 13 14 next


Further publications can be found at: http://www.prismmodelchecker.org/publications.php