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.
11 publications:
-
[KNPS20]
Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos.
PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time.
In Proc. 32nd International Conference on Computer Aided Verification (CAV'20), volume 12225 of LNCS, pages 475-487, Springer.
July 2020.
[pdf]
[bib]
[Tool paper describing the new features in PRISM-games 3.0.]
-
[KNP11]
Marta Kwiatkowska, Gethin Norman and David Parker.
PRISM 4.0: Verification of Probabilistic Real-time Systems.
In Proc. 23rd International Conference on Computer Aided Verification (CAV'11), volume 6806 of LNCS, pages 585-591, Springer.
July 2011.
[pdf]
[bib]
[Tool paper describing PRISM 4.0.]
-
[Par23]
David Parker.
Multi-Agent Verification and Control with Probabilistic Model Checking.
In Proc. 20th International Conference on Quantitative Evaluation of SysTems (QEST'23), volume 14287 of LNCS, pages 1-9, Springer.
September 2023.
[pdf]
[bib]
[Summarises advances in probabilistic model checking for stochastic games, as implemented in PRISM-games, and discusses its applicability to multi-agent systems.]
-
[KNP22]
Marta Kwiatkowska, Gethin Norman and David Parker.
Probabilistic Model Checking and Autonomy.
Annual Review of Control, Robotics, and Autonomous Systems, 5, pages 385-410, Annual Reviews.
May 2022.
[pdf]
[bib]
[Gives an overview of probabilistic model checking as applied to the context of robotics and autonomous systems.]
-
[KNP17]
Marta Kwiatkowska, Gethin Norman and David Parker.
Probabilistic Model Checking: Advances and Applications.
In R. Drechsler (editor), Formal System Verification, pages 73-121, Springer.
June 2017.
[pdf]
[bib]
[Provides an introduction to probabilistic model checking, including coverage of some recent advances in the field and a wide variety of examples and applications.]
-
[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.]
