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

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

1 2 3 ... 17 18 19 next

  1. Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian: Formal reliability analysis of redundancy architectures (2019)
  2. Sproston, Jeremy: Verification and control for probabilistic hybrid automata with finite bisimulations (2019)
  3. Andrei, Oana; Calder, Muffy: Data-driven modelling and probabilistic analysis of interactive software usage (2018)
  4. Anticoli, Linda; Ghahi, Masoud Gharahi: Modeling tripartite entanglement in quantum protocols using evolving entangled hypergraphs (2018)
  5. Baier, Christel; de Alfaro, Luca; Forejt, Vojtěch; Kwiatkowska, Marta: Model checking probabilistic systems (2018)
  6. Bart, Anicet; Delahaye, Benoît; Fournier, Paulin; Lime, Didier; Monfroy, Éric; Truchet, Charlotte: Reachability in parametric interval Markov chains using constraints (2018)
  7. Basin, David; Cremers, Cas; Meadows, Catherine: Model checking security protocols (2018)
  8. Bortolussi, Luca; Lanciani, Roberta; Nenzi, Laura: Model checking Markov population models by stochastic approximations (2018)
  9. Chatzieleftheriou, G.; Katsaros, P.: Abstract model repair for probabilistic systems (2018)
  10. Chu, Dominique: Performance limits and trade-offs in entropy-driven biochemical computers (2018)
  11. Dennis, Louise A.; Fisher, Michael; Webster, Matt: Two-stage agent program verification (2018)
  12. de Putter, Sander; Wijs, Anton: A formal verification technique for behavioural model-to-model transformations (2018)
  13. Eisentraut, Christian; Hermanns, Holger; Schuster, Johann; Turrini, Andrea; Zhang, Lijun: The quest for minimal quotients for probabilistic and Markov automata (2018)
  14. Gerhold, Marcus; Stoelinga, Mariëlle: Model-based testing of probabilistic systems (2018)
  15. Gutierrez, Julian; Perelli, Giuseppe; Wooldridge, Michael: Imperfect information in reactive modules games (2018)
  16. Haddad, Serge; Monmege, Benjamin: Interval iteration algorithm for MDPs and IMDPs (2018)
  17. Jha, Susmit; Raman, Vasumathi; Sadigh, Dorsa; Seshia, Sanjit A.: Safe autonomy under perception uncertainty using chance-constrained temporal logic (2018)
  18. Jing, Yaping; Miner, Andrew S.: Computation tree measurement language (CTML) (2018)
  19. Jovanović, Aleksandra; Kwiatkowska, Marta: Parameter synthesis for probabilistic timed automata using stochastic game abstractions (2018)
  20. Riveret, Régis; Baroni, Pietro; Gao, Yang; Governatori, Guido; Rotolo, Antonino; Sartor, Giovanni: A labelling framework for probabilistic argumentation (2018)

1 2 3 ... 17 18 19 next


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