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

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

1 2 3 ... 15 16 17 next

  1. de Putter, Sander; Wijs, Anton: A formal verification technique for behavioural model-to-model transformations (2018)
  2. Gerhold, Marcus; Stoelinga, Mariëlle: Model-based testing of probabilistic systems (2018)
  3. Alechina, Natasha; Bulling, Nils; Logan, Brian; Nguyen, Hoang Nga: The virtues of idleness: A decidable fragment of resource agent logic (2017)
  4. Bakir, Mehmet Emin; Gheorghe, Marian; Konur, Savas; Stannett, Mike: Comparative analysis of statistical model checking tools (2017)
  5. 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)
  6. Bian, Gaoang; Abate, Alessandro: On the relationship between bisimulation and trace equivalence in an approximate probabilistic context (2017)
  7. 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)
  8. Češka, Milan; Dannenberg, Frits; Paoletti, Nicola; Kwiatkowska, Marta; Brim, Luboš: Precise parameter synthesis for stochastic biochemical systems (2017)
  9. Chatterjee, Krishnendu; Křetínská, Zuzana; Křetínský, Jan: Unifying two views on multiple mean-payoff objectives in Markov decision processes (2017)
  10. Chu, Dominique: Limited by sensing -- a minimal stochastic model of the lag-phase during diauxic growth (2017)
  11. Daca, Przemysław; Henzinger, Thomas A.; Křetínský, Jan; Petrov, Tatjana: Faster statistical model checking for unbounded temporal properties (2017)
  12. da Costa Cavalheiro, Simone André; Foss, Luciana; Ribeiro, Leila: Theorem proving graph grammars with attributes and negative application conditions (2017)
  13. Esmaeil Zadeh Soudjani, Sadegh; Abate, Alessandro; Majumdar, Rupak: Dynamic Bayesian networks for formal verification of structured stochastic processes (2017)
  14. Feng, Yuan; Zhang, Lijun: Precisely deciding CSL formulas through approximate model checking for CTMCs (2017)
  15. Hahn, Ernst Moritz; Schewe, Sven; Turrini, Andrea; Zhang, Lijun: Synthesising strategy improvement and recursive algorithms for solving 2.5 player parity games (2017)
  16. Hansen, Eric A.: Error bounds for stochastic shortest path problems (2017)
  17. Hashemi, Vahid: Reformulation of the linear program for completely ergodic MDPs with average cost criteria (2017)
  18. Hoque, Khaza Anuarul; Mohamed, Otmane Ait; Savaria, Yvon: Formal analysis of SEU mitigation for early dependability and performability analysis of FPGA-based space applications (2017)
  19. Jovanović, Aleksandra; Kwiatkowska, Marta; Norman, Gethin; Peyras, Quentin: Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata (2017)
  20. Juan F. Pérez; Daniel F. Silva; Julio C. Góez; Andrés Sarmiento; Andrés Sarmiento-Romero; Raha Akhavan-Tabatabaei; Germán Riaño: Algorithm 972: jMarkov: An Integrated Framework for Markov Chain Modeling (2017) misc

1 2 3 ... 15 16 17 next


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