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

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

1 2 3 ... 16 17 18 next

  1. Andrei, Oana; Calder, Muffy: Data-driven modelling and probabilistic analysis of interactive software usage (2018)
  2. Baier, Christel; de Alfaro, Luca; Forejt, Vojtěch; Kwiatkowska, Marta: Model checking probabilistic systems (2018)
  3. Bart, Anicet; Delahaye, Beno^ıt; Fournier, Paulin; Lime, Didier; Monfroy, Éric; Truchet, Charlotte: Reachability in parametric interval Markov chains using constraints (2018)
  4. Basin, David; Cremers, Cas; Meadows, Catherine: Model checking security protocols (2018)
  5. Bortolussi, Luca; Lanciani, Roberta; Nenzi, Laura: Model checking Markov population models by stochastic approximations (2018)
  6. Chatzieleftheriou, G.; Katsaros, P.: Abstract model repair for probabilistic systems (2018)
  7. Chu, Dominique: Performance limits and trade-offs in entropy-driven biochemical computers (2018)
  8. de Putter, Sander; Wijs, Anton: A formal verification technique for behavioural model-to-model transformations (2018)
  9. Eisentraut, Christian; Hermanns, Holger; Schuster, Johann; Turrini, Andrea; Zhang, Lijun: The quest for minimal quotients for probabilistic and Markov automata (2018)
  10. Gerhold, Marcus; Stoelinga, Mariëlle: Model-based testing of probabilistic systems (2018)
  11. Gutierrez, Julian; Perelli, Giuseppe; Wooldridge, Michael: Imperfect information in reactive modules games (2018)
  12. Haddad, Serge; Monmege, Benjamin: Interval iteration algorithm for MDPs and IMDPs (2018)
  13. Jha, Susmit; Raman, Vasumathi; Sadigh, Dorsa; Seshia, Sanjit A.: Safe autonomy under perception uncertainty using chance-constrained temporal logic (2018)
  14. Jovanović, Aleksandra; Kwiatkowska, Marta: Parameter synthesis for probabilistic timed automata using stochastic game abstractions (2018)
  15. Riveret, Régis; Baroni, Pietro; Gao, Yang; Governatori, Guido; Rotolo, Antonino; Sartor, Giovanni: A labelling framework for probabilistic argumentation (2018)
  16. Sardar, Muhammad Usama; Afaq, Nida; Hasan, Osman; Hoque, Khaza Anuarul: Towards probabilistic formal analysis of SATS-simultaneously moving aircraft (SATS-SMA) (2018)
  17. Alechina, Natasha; Bulling, Nils; Logan, Brian; Nguyen, Hoang Nga: The virtues of idleness: A decidable fragment of resource agent logic (2017)
  18. Bakir, Mehmet Emin; Gheorghe, Marian; Konur, Savas; Stannett, Mike: Comparative analysis of statistical model checking tools (2017)
  19. Barbuti, Roberto; Bove, Pasquale; Milazzo, Paolo; Pardini, Giovanni: Applications of P systems in population biology and ecology: the cases of MPP and APP systems (2017)
  20. Bian, Gaoang; Abate, Alessandro: On the relationship between bisimulation and trace equivalence in an approximate probabilistic context (2017)

1 2 3 ... 16 17 18 next


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