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

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

1 2 3 ... 20 21 22 next

  1. Fearnley, John; Gairing, Martin; Mnich, Matthias; Savani, Rahul: Reachability switching games (2021)
  2. Gleason, Joseph D.; Vinod, Abraham P.; Oishi, Meeko M. K.: Lagrangian approximations for stochastic reachability of a target tube (2021)
  3. Junges, Sebastian; Katoen, Joost-Pieter; Pérez, Guillermo A.; Winkler, Tobias: The complexity of reachability in parametric Markov decision processes (2021)
  4. Sproston, Jeremy: Probabilistic timed automata with clock-dependent probabilities (2021)
  5. Baier, Christel; Hensel, Christian; Hutschenreiter, Lisa; Junges, Sebastian; Katoen, Joost-Pieter; Klein, Joachim: Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination (2020)
  6. Bersani, Marcello M.; Soldo, Matteo; Menghi, Claudio; Pelliccione, Patrizio; Rossi, Matteo: PuRSUE -- from specification of robotic environments to synthesis of controllers (2020)
  7. Fahrenberg, Uli; Legay, Axel; Quaas, Karin: Computing branching distances with quantitative games (2020)
  8. Fraser, Douglas; Giaquinta, Ruben; Hoffmann, Ruth; Ireland, Murray; Miller, Alice; Norman, Gethin: Collaborative models for autonomous systems controller synthesis (2020)
  9. Gainer, Paul; Linker, Sven; Dixon, Clare; Hustadt, Ullrich; Fisher, Michael: Multi-scale verification of distributed synchronisation (2020)
  10. Hartmanns, Arnd; Junges, Sebastian; Katoen, Joost-Pieter; Quatmann, Tim: Multi-cost bounded tradeoff analysis in MDP (2020)
  11. Jamroga, Wojciech; Konikowska, Beata; Kurpiewski, Damian; Penczek, Wojciech: Multi-valued verification of strategic ability (2020)
  12. Křetínský, Jan; Meggendorfer, Tobias: Of cores: a partial-exploration framework for Markov decision processes (2020)
  13. Lavaei, Abolfazl; Khaled, Mahmoud; Soudjani, Sadegh; Zamani, Majid: AMYTISS: a parallelized tool on automated controller synthesis for large-scale stochastic systems (2020)
  14. Mathur, Umang; Bauer, Matthew S.; Chadha, Rohit; Sistla, A. Prasad; Viswanathan, Mahesh: Exact quantitative probabilistic model checking through rational search (2020)
  15. Michaliszyn, Jakub; Otop, Jan: Non-deterministic weighted automata evaluated over Markov chains (2020)
  16. Tang, Qiyi; van Breugel, Franck: Deciding probabilistic bisimilarity distance one for probabilistic automata (2020)
  17. Thiagarajan, P. S.; Yang, Shaofa: A theory of distributed Markov chains (2020)
  18. Zaw, Hein Htoo; Hlaing, Swe Zin: Verifying the gaming strategy of self-learning game by using PRISM-games (2020)
  19. Aichernig, Bernhard K.; Tappler, Martin: Probabilistic black-box reachability checking (extended version) (2019)
  20. Bartocci, Ezio; Kovács, Laura; Stankovič, Miroslav: Automatic generation of moment-based invariants for prob-solvable loops (2019)

1 2 3 ... 20 21 22 next


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