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

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

1 2 3 ... 12 13 14 next

  1. Bohy, Aaron; Bruyère, Véronique; Raskin, Jean-François; Bertrand, Nathalie: Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes (2017)
  2. Češka, Milan; Dannenberg, Frits; Paoletti, Nicola; Kwiatkowska, Marta; Brim, Luboš: Precise parameter synthesis for stochastic biochemical systems (2017)
  3. Chatterjee, Krishnendu; Křetínská, Zuzana; Křetínský, Jan: Unifying two views on multiple mean-payoff objectives in Markov decision processes (2017)
  4. Chu, Dominique: Limited by sensing -- a minimal stochastic model of the lag-phase during diauxic growth (2017)
  5. Esmaeil Zadeh Soudjani, Sadegh; Abate, Alessandro; Majumdar, Rupak: Dynamic Bayesian networks for formal verification of structured stochastic processes (2017)
  6. Feng, Yuan; Zhang, Lijun: Precisely deciding CSL formulas through approximate model checking for CTMCs (2017)
  7. Hansen, Eric A.: Error bounds for stochastic shortest path problems (2017)
  8. Bortolussi, Luca; Milios, Dimitrios; Sanguinetti, Guido: Smoothed model checking for uncertain continuous-time Markov chains (2016)
  9. Cardelli, Luca; Kwiatkowska, Marta; Whitby, Max: Chemical reaction network designs for asynchronous logic circuits (2016)
  10. Cardelli, Luca; Tribastone, Mirco; Tschaikowski, Max; Vandin, Andrea: Symbolic computation of differential equivalences (2016)
  11. Chatterjee, Krishnendu; Chmelík, Martin; Gupta, Raghav; Kanodia, Ayush: Optimal cost almost-sure reachability in POMDPs (2016)
  12. Chatterjee, Krishnendu; Chmelík, Martin; Tracol, Mathieu: What is decidable about partially observable Markov decision processes with $\omega$-regular objectives (2016)
  13. Chen, Taolue; Primiero, Giuseppe; Raimondi, Franco; Rungta, Neha: A computationally grounded, weighted doxastic logic (2016)
  14. Esparza, Javier; Křetínský, Jan; Sickert, Salomon: From LTL to deterministic automata. A safraless compositional approach (2016)
  15. Ferrer Fioriti, Luis María; Hashemi, Vahid; Hermanns, Holger; Turrini, Andrea: Deciding probabilistic automata weak bisimulation: theory and practice (2016)
  16. Jegourel, Cyrille; Legay, Axel; Sedwards, Sean: Command-based importance sampling for statistical model checking (2016)
  17. Kamaleson, Nishanthan; Parker, David; Rowe, Jonathan E.: Finite-horizon bisimulation minimisation for probabilistic systems (2016)
  18. Kirwan, Ryan; Miller, Alice; Porr, Bernd: Model checking learning agent systems using Promela with embedded C code and abstraction (2016)
  19. Kubota, Takahiro; Kakutani, Yoshihiko; Kato, Go; Kawano, Yasuhito; Sakurada, Hideki: Semi-automated verification of security proofs of quantum cryptographic protocols (2016)
  20. Lakin, Matthew R.; Stefanovic, Darko; Phillips, Andrew: Modular verification of chemical reaction network encodings via serializability analysis (2016)

1 2 3 ... 12 13 14 next


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