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

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

1 2 3 ... 15 16 17 next

  1. Chatzieleftheriou, G.; Katsaros, P.: Abstract model repair for probabilistic systems (2018)
  2. de Putter, Sander; Wijs, Anton: A formal verification technique for behavioural model-to-model transformations (2018)
  3. Gerhold, Marcus; Stoelinga, Mariëlle: Model-based testing of probabilistic systems (2018)
  4. Haddad, Serge; Monmege, Benjamin: Interval iteration algorithm for MDPs and IMDPs (2018)
  5. Jha, Susmit; Raman, Vasumathi; Sadigh, Dorsa; Seshia, Sanjit A.: Safe autonomy under perception uncertainty using chance-constrained temporal logic (2018)
  6. Jovanović, Aleksandra; Kwiatkowska, Marta: Parameter synthesis for probabilistic timed automata using stochastic game abstractions (2018)
  7. Sardar, Muhammad Usama; Afaq, Nida; Hasan, Osman; Hoque, Khaza Anuarul: Towards probabilistic formal analysis of SATS-simultaneously moving aircraft (SATS-SMA) (2018)
  8. Alechina, Natasha; Bulling, Nils; Logan, Brian; Nguyen, Hoang Nga: The virtues of idleness: A decidable fragment of resource agent logic (2017)
  9. Bakir, Mehmet Emin; Gheorghe, Marian; Konur, Savas; Stannett, Mike: Comparative analysis of statistical model checking tools (2017)
  10. 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)
  11. Bian, Gaoang; Abate, Alessandro: On the relationship between bisimulation and trace equivalence in an approximate probabilistic context (2017)
  12. 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)
  13. Češka, Milan; Dannenberg, Frits; Paoletti, Nicola; Kwiatkowska, Marta; Brim, Luboš: Precise parameter synthesis for stochastic biochemical systems (2017)
  14. Chatterjee, Krishnendu; Křetínská, Zuzana; Křetínský, Jan: Unifying two views on multiple mean-payoff objectives in Markov decision processes (2017)
  15. Chu, Dominique: Limited by sensing -- a minimal stochastic model of the lag-phase during diauxic growth (2017)
  16. Daca, Przemysław; Henzinger, Thomas A.; Křetínský, Jan; Petrov, Tatjana: Faster statistical model checking for unbounded temporal properties (2017)
  17. da Costa Cavalheiro, Simone André; Foss, Luciana; Ribeiro, Leila: Theorem proving graph grammars with attributes and negative application conditions (2017)
  18. Esmaeil Zadeh Soudjani, Sadegh; Abate, Alessandro; Majumdar, Rupak: Dynamic Bayesian networks for formal verification of structured stochastic processes (2017)
  19. Esmaeil Zadeh Soudjani, Sadegh; Majumdar, Rupak: Controller synthesis for reward collecting Markov processes in continuous space (2017)
  20. Feng, Yuan; Zhang, Lijun: Precisely deciding CSL formulas through approximate model checking for CTMCs (2017)

1 2 3 ... 15 16 17 next

Further publications can be found at: