Selected PRISM Publications
The following is a selection of PRISM-related papers
for those wanting to learn more about the tool, its underlying techniques
and ongoing work in the area.
See also the lists of
all PRISM papers,
the full PRISM bibliography
and
external PRISM papers.
14 publications:
-
[KNP10c]
Marta Kwiatkowska, Gethin Norman and David Parker.
Advances and Challenges of Probabilistic Model Checking.
In Proc. 48th Annual Allerton Conference on Communication, Control and Computing, pages 1691-1698, IEEE Press. Invited paper.
October 2010.
[pdf]
[bib]
[Gives a high-level overview of probabilistic model checking and PRISM; and surveys some current recent directions.]
-
[NP14]
Gethin Norman and David Parker.
Quantitative Verification: Formal Guarantees for Timeliness, Reliability and Performance.
A report by the London Mathematical Society and the Smith Institute. Edited by Robert Leese and Tom Melham.
2014.
[pdf]
[bib]
[Gives a short, accessible introduction to quantitative verification, with a focus on model checking for timed and probabilistic systems.]
-
[KNP07a]
Marta Kwiatkowska, Gethin Norman and David Parker.
Stochastic Model Checking.
In M. Bernardo and J. Hillston (editors), Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07), volume 4486 of Lecture Notes in Computer Science (Tutorial Volume), pages 220-270, Springer.
June 2007.
[pdf]
[bib]
[Tutorial paper covering probabilistic model checking of DTMCs/CTMCs and PRISM.]
-
[FKNP11]
Vojtěch Forejt, Marta Kwiatkowska, Gethin Norman and David Parker.
Automated Verification Techniques for Probabilistic Systems.
In M. Bernardo and V. Issarny (editors), Formal Methods for Eternal Networked Software Systems (SFM'11), volume 6659 of LNCS, pages 53-113, Springer.
June 2011.
[pdf]
[bib]
[Tutorial paper on probabilistic model checking, focusing on verification techniques for MDPs, accompanied by case studies and examples for PRISM.]
-
[NPS13]
Gethin Norman, David Parker and Jeremy Sproston.
Model Checking for Probabilistic Timed Automata.
Formal Methods in System Design, 43(2), pages 164-190, Springer.
September 2013.
[pdf]
[bib]
[Survey/tutorial paper on probabilistic timed automata and techniques for their verification, and two illustrative case studies.]
-
[KNP10a]
Marta Kwiatkowska, Gethin Norman and David Parker.
Probabilistic Model Checking for Systems Biology.
In M. Sriram Iyengar (editor), Symbolic Systems Biology, pages 31-59, Jones and Bartlett.
May 2010.
[pdf]
[bib]
[Tutorial on the application of probabilistic model checking and PRISM to systems biology, including an illustrative case study (FGF) and reader exercises.]
-
[KT14]
Marta Kwiatkowska and Chris Thachuk.
Probabilistic Model Checking for Biology.
In Software Safety and Security, IOS Press.
2014.
[pdf]
[bib]
[A tutorial on the application of probabilistic model checking and PRISM to biological systems, including examples of DNA computation.]
-
[FKP12]
Vojtěch Forejt, Marta Kwiatkowska and David Parker.
Pareto Curves for Probabilistic Model Checking.
In Proc. 10th International Symposium on Automated Technology for Verification and Analysis (ATVA'12), volume 7561 of LNCS, pages 317-332, Springer.
October 2012.
[pdf]
[bib]
[Describes new techniques for multi-objective probabilistic model checking using Pareto curves, implemented in PRISM.]
-
[GR12]
Sergio Giro and Markus Rabe.
Verification of Partial-Information Probabilistic Systems using Counterexample-Guided Refinements.
In Proc. 10th International Symposium on Automated Technology for Verification and Analysis (ATVA'12), volume 7561 of LNCS, pages 333-348, Springer.
October 2012.
[pdf]
[bib]
[Describes new techniques for model checking MDPs under partial-information schedulers, implemented in an extension of PRISM.]
-
[CFK+12]
Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, David Parker and Aistis Simaitis.
Automatic Verification of Competitive Stochastic Systems.
In Proc. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12), volume 7214 of LNCS, pages 315-330, Springer.
March 2012.
[pdf]
[bib]
[Introduces model checking techniques for stochastic multi-player games, implemented in the PRISM-games tool.]
-
[CDKM12b]
Taolue Chen, Marco Diciolla, Marta Kwiatkowska and Alexandru Mereacre.
Quantitative Verification of Implantable Cardiac Pacemakers.
In Proc. 33rd IEEE Real-Time Systems Symposium (RTSS'12), pages 263-272, IEEE.
December 2012.
[pdf]
[Proposes quantitative verification techniques for the analysis of pacemaker software, using the tools PRISM and MATLAB.]
-
[LPC+12]
Matthew Lakin, David Parker, Luca Cardelli, Marta Kwiatkowska and Andrew Phillips.
Design and Analysis of DNA Strand Displacement Devices using Probabilistic Model Checking.
Journal of the Royal Society Interface, 9(72), pages 1470-1485, The Royal Society.
July 2012.
[pdf]
[bib]
[Analyses correctness, reliability and performance of DNA computing designs using PRISM and DSD.]