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

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

1 2 3 ... 16 17 18 next

  1. Baier, Christel; de Alfaro, Luca; Forejt, Vojtěch; Kwiatkowska, Marta: Model checking probabilistic systems (2018)
  2. Basin, David; Cremers, Cas; Meadows, Catherine: Model checking security protocols (2018)
  3. Chatzieleftheriou, G.; Katsaros, P.: Abstract model repair for probabilistic systems (2018)
  4. Chu, Dominique: Performance limits and trade-offs in entropy-driven biochemical computers (2018)
  5. de Putter, Sander; Wijs, Anton: A formal verification technique for behavioural model-to-model transformations (2018)
  6. Gerhold, Marcus; Stoelinga, Mariëlle: Model-based testing of probabilistic systems (2018)
  7. Gutierrez, Julian; Perelli, Giuseppe; Wooldridge, Michael: Imperfect information in reactive modules games (2018)
  8. Haddad, Serge; Monmege, Benjamin: Interval iteration algorithm for MDPs and IMDPs (2018)
  9. Jha, Susmit; Raman, Vasumathi; Sadigh, Dorsa; Seshia, Sanjit A.: Safe autonomy under perception uncertainty using chance-constrained temporal logic (2018)
  10. Jovanović, Aleksandra; Kwiatkowska, Marta: Parameter synthesis for probabilistic timed automata using stochastic game abstractions (2018)
  11. Riveret, Régis; Baroni, Pietro; Gao, Yang; Governatori, Guido; Rotolo, Antonino; Sartor, Giovanni: A labelling framework for probabilistic argumentation (2018)
  12. Sardar, Muhammad Usama; Afaq, Nida; Hasan, Osman; Hoque, Khaza Anuarul: Towards probabilistic formal analysis of SATS-simultaneously moving aircraft (SATS-SMA) (2018)
  13. Alechina, Natasha; Bulling, Nils; Logan, Brian; Nguyen, Hoang Nga: The virtues of idleness: A decidable fragment of resource agent logic (2017)
  14. Bakir, Mehmet Emin; Gheorghe, Marian; Konur, Savas; Stannett, Mike: Comparative analysis of statistical model checking tools (2017)
  15. 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)
  16. Bian, Gaoang; Abate, Alessandro: On the relationship between bisimulation and trace equivalence in an approximate probabilistic context (2017)
  17. 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)
  18. Češka, Milan; Dannenberg, Frits; Paoletti, Nicola; Kwiatkowska, Marta; Brim, Luboš: Precise parameter synthesis for stochastic biochemical systems (2017)
  19. Chatterjee, Krishnendu; Křetínská, Zuzana; Křetínský, Jan: Unifying two views on multiple mean-payoff objectives in Markov decision processes (2017)
  20. Chu, Dominique: Limited by sensing -- a minimal stochastic model of the lag-phase during diauxic growth (2017)

1 2 3 ... 16 17 18 next


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