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

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

1 2 3 ... 18 19 20 next

  1. Baier, Christel; Hensel, Christian; Hutschenreiter, Lisa; Junges, Sebastian; Katoen, Joost-Pieter; Klein, Joachim: Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination (2020)
  2. Michaliszyn, Jakub; Otop, Jan: Non-deterministic weighted automata evaluated over Markov chains (2020)
  3. Tang, Qiyi; van Breugel, Franck: Deciding probabilistic bisimilarity distance one for probabilistic automata (2020)
  4. Aichernig, Bernhard K.; Tappler, Martin: Probabilistic black-box reachability checking (extended version) (2019)
  5. Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian: Formal reliability analysis of redundancy architectures (2019)
  6. Camacho, Carlos; Llana, Luis; Núñez, Alberto; Bravetti, Mario: Probabilistic software product lines (2019)
  7. Cardelli, Luca; Tribastone, Mirco; Tschaikowski, Max; Vandin, Andrea: Symbolic computation of differential equivalences (2019)
  8. Chatterjee, Krishnendu; Henzinger, Thomas A.; Otop, Jan: Quantitative automata under probabilistic semantics (2019)
  9. Gutierrez, Julian; Harrenstein, Paul; Perelli, Giuseppe; Wooldridge, Michael: Nash equilibrium and bisimulation invariance (2019)
  10. Jamroga, Wojciech; Malvone, Vadim; Murano, Aniello: Natural strategic ability (2019)
  11. Liu, Si; Ölveczky, Peter Csaba; Wang, Qi; Gupta, Indranil; Meseguer, José: Read atomic transactions with prevention of lost updates: ROLA and its formal analysis (2019)
  12. Ouadjaout, Abdelraouf; Miné, Antoine: Quantitative static analysis of communication protocols using abstract Markov chains (2019)
  13. Sproston, Jeremy: Verification and control for probabilistic hybrid automata with finite bisimulations (2019)
  14. Wang, Yu; Roohi, Nima; West, Matthew; Viswanathan, Mahesh; Dullerud, Geir E.: Statistical verification of PCTL using antithetic and stratified samples (2019)
  15. Andrei, Oana; Calder, Muffy: Data-driven modelling and probabilistic analysis of interactive software usage (2018)
  16. Anticoli, Linda; Ghahi, Masoud Gharahi: Modeling tripartite entanglement in quantum protocols using evolving entangled hypergraphs (2018)
  17. Baier, Christel; de Alfaro, Luca; Forejt, Vojtěch; Kwiatkowska, Marta: Model checking probabilistic systems (2018)
  18. Bart, Anicet; Delahaye, Benoît; Fournier, Paulin; Lime, Didier; Monfroy, Éric; Truchet, Charlotte: Reachability in parametric interval Markov chains using constraints (2018)
  19. Basin, David; Cremers, Cas; Meadows, Catherine: Model checking security protocols (2018)
  20. Bortolussi, Luca; Lanciani, Roberta; Nenzi, Laura: Model checking Markov population models by stochastic approximations (2018)

1 2 3 ... 18 19 20 next


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