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

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

1 2 3 ... 21 22 23 next

  1. Stankovič, Miroslav; Bartocci, Ezio; Kovács, Laura: Moment-based analysis of Bayesian network properties (2022)
  2. Archibald, Blair; Kulcsár, Géza; Sevegnani, Michele: A tale of two graph models: a case study in wireless sensor networks (2021)
  3. Benouhiba, Toufik: A multi-level refinement approach for structural synthesis of optimal probabilistic models (2021)
  4. Bentriou, Mahmoud; Ballarini, Paolo; Cournède, Paul-Henry: Automaton-ABC: a statistical method to estimate the probability of spatio-temporal properties for parametric Markov population models (2021)
  5. Bonchi, Filippo; Silva, Alexandra; Sokolova, Ana: Distribution bisimilarity via the power of convex algebras (2021)
  6. Češka, Milan; Hensel, Christian; Junges, Sebastian; Katoen, Joost-Pieter: Counterexample-guided inductive synthesis for probabilistic systems (2021)
  7. Dubslaff, Clemens; Koopmann, Patrick; Turhan, Anni-Yasmin: Enhancing probabilistic model checking with ontologies (2021)
  8. Evangelidis, Alexandros; Parker, David: Quantitative verification of Kalman filters (2021)
  9. Fearnley, John; Gairing, Martin; Mnich, Matthias; Savani, Rahul: Reachability switching games (2021)
  10. Getir Yaman, Sinem; Pavese, Esteban; Grunske, Lars: Quantitative verification of stochastic regular expressions (2021)
  11. Gleason, Joseph D.; Vinod, Abraham P.; Oishi, Meeko M. K.: Lagrangian approximations for stochastic reachability of a target tube (2021)
  12. Junges, Sebastian; Katoen, Joost-Pieter; Pérez, Guillermo A.; Winkler, Tobias: The complexity of reachability in parametric Markov decision processes (2021)
  13. Lanotte, Ruggero; Merro, Massimo; Tini, Simone: A probabilistic calculus of cyber-physical systems (2021)
  14. Mitani, Yo; Kobayashi, Naoki; Tsukada, Takeshi: A probabilistic higher-order fixpoint logic (2021)
  15. Sproston, Jeremy: Probabilistic timed automata with clock-dependent probabilities (2021)
  16. Stankaitis, Paulius; Iliasov, Alexei; Kobayashi, Tsutomu; Aït-Ameur, Yamine; Ishikawa, Fuyuki; Romanovsky, Alexander: A refinement-based development of a distributed signalling system (2021)
  17. Tappler, Martin; Aichernig, Bernhard K.; Bacci, Giovanni; Eichlseder, Maria; Larsen, Kim G.: (L^\ast)-based learning of Markov decision processes (extended version) (2021)
  18. Wißmann, Thorsten; Deifel, Hans-Peter; Milius, Stefan; Schröder, Lutz: From generic partition refinement to weighted tree automata minimization (2021)
  19. Baier, Christel; Hensel, Christian; Hutschenreiter, Lisa; Junges, Sebastian; Katoen, Joost-Pieter; Klein, Joachim: Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination (2020)
  20. Bersani, Marcello M.; Soldo, Matteo; Menghi, Claudio; Pelliccione, Patrizio; Rossi, Matteo: PuRSUE -- from specification of robotic environments to synthesis of controllers (2020)

1 2 3 ... 21 22 23 next


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