PRISM Publications

The following is a list of all PRISM-related papers authored or co-authored by members of the PRISM team.

See also the lists of selected PRISM papers, the full PRISM bibliography and external PRISM papers.

Sort by: date, type, title, subject

Underlying techniques in PRISM
Extensions and adaptions to PRISM
Tool/language connections to PRISM
Case studies using PRISM
PRISM tool papers
PRISM-related tutorials and surveys
Others

239 publications:

Underlying techniques in PRISM (66)

[KNPS22b] Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos. Symbolic Verification and Strategy Synthesis for Turn-based Stochastic Games. In Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, volume 13660 of LNCS, Springer. December 2022. [pdf] [bib] [Investigates symbolic model checking of turn-based stochastic games, implemented in PRISM-games.]
[KNPS22] Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos. Correlated Equilibria and Fairness in Concurrent Stochastic Games. In Proc. 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'22), volume 13244 of LNCS, pages 60–78, Springer. April 2022. [pdf] [bib] [Presents novel techniques for synthesising equilibria in stochastic games, implemented in PRISM-games.]
[KNPS21] Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos. Automatic Verification of Concurrent Stochastic Systems. Formal Methods in System Design, 58, pages 188–250, Springer. 2021. [pdf] [bib] [Proposes verification techniques for concurrent stochastic games, and implements and evaluates them in an extension of PRISM-games. ]
[San21] Gabriel Santos. Automatic Verification and Strategy Synthesis for Zero-sum and Equilibria Properties of Concurrent Stochastic Games. Ph.D. thesis, Department of Computer Science, University of Oxford. March 2021. [pdf] [bib] [Develops a variety of verification and strategy synthesis techniques for concurrent stochastic games, implemented in PRISM-games.]
[KNPS20b] Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos. Multi-player Equilibria Verification for Concurrent Stochastic Games. In Proc. 17th International Conference on Quantitative Evaluation of SysTems (QEST'20), Springer. August 2020. [pdf] [bib] [Presents techniques for model checking CSGs against equilibria-based properties over multiple coalitions, implemented in PRISM-games.]
[KNP19] Marta Kwiatkowska, Gethin Norman and David Parker. Verification and Control of Turn-Based Probabilistic Real-Time Games. In The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy (Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday), volume 11760 of LNCS, pages 379-396, Springer. November 2019. [pdf] [bib] [Proposes techniques for verifying probabilistic real-time games building on methods implemented in PRISM-games.]
[KNPS19] Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos. Equilibria-based Probabilistic Model Checking for Concurrent Stochastic Games. In Proc. 23rd International Symposium on Formal Methods (FM'19), volume 11800 of LNCS, pages 298-315, Springer. October 2019. [pdf] [bib] [Develops verification methods for stochastic games using Nash equilibria, implemented in PRISM-games.]
[KNPS18] Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos. Automated Verification of Concurrent Stochastic Games. In Proc. 15th International Conference on Quantitative Evaluation of SysTems (QEST'18), volume 11024 of LNCS, pages 223-239, Springer. September 2018. [pdf] [bib] [Proposes verification techniques for concurrent stochastic games, and implements and evaluates them in an extension of PRISM-games.]
[BKW17] Nicolas Basset, Marta Kwiatkowska and Clemens Wiltsche. Compositional Strategy Synthesis for Stochastic Games with Multiple Objectives. Information and Computation, 261(3), pages 536-587. 2017. [pdf] [bib] [Proposes multi-objective strategy synthesis techniques for stochastic games, along with a compositional assume-guarantee strategy synthesis framework.]
[KNP17b] Marta Kwiatkowska, Gethin Norman and David Parker. Symbolic Verification and Strategy Synthesis for Linearly-Priced Probabilistic Timed Automata. In Models, Algorithms, Logics and Tools, volume 10460 of LNCS, pages 289-309, Springer. August 2017. [pdf] [bib] [Proposes novel symbolic techniques for verification and optimal strategy synthesis for priced probabilistic timed automata ]
[BKLPW17] Christel Baier, Joachim Klein, Linda Leuschner, David Parker and Sascha Wunderlich. Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes. In Proc. 28th International Conference on Computer Aided Verification (CAV'17), volume 10426 of LNCS, pages 160-180, Springer. July 2017. [pdf] [bib] [Proposes "interval iteration" techniques for deriving more accurate bounds on the results of probabilistic model checking, and implements them in PRISM.]
[Dan16] Frits Dannenberg. Modelling and verification for DNA nanotechnology. Ph.D. thesis, Department of Computer Science, University of Oxford. 2016. [pdf] [bib] [Develops models of DNA nanotechnology designs, based on continuous-time Markov chains, and associated model checking techniques.]
[vEJPV16] Christian von Essen, Barbara Jobstmann, David Parker and Rahul Varshneya. Synthesizing Efficient Systems in Probabilistic Environments. Acta Informatica, 53(4), pages 425–457, Springer. June 2016. [pdf] [bib] [Proposes efficient techniques for synthesising strategies in Markov decision processes against ratio objectives, implemented in an extension of PRISM.]
[KPR16] Nishanthan Kamaleson, David Parker and Jonathan E. Rowe. Finite-Horizon Bisimulation Minimisation for Probabilistic Systems. In Proc. 2016 International Symposium on Model Checking of Software (SPIN'16), volume 9641 of LNCS, pages 147-164, Springer. April 2016. [pdf] [bib] [Proposes a finite-horizon variant of probabilistic bisimulation and implements various associated minimisation algorithms in an extension of PRISM.]
[DFK+15] Klaus Draeger, Vojtěch Forejt, Marta Kwiatkowska, David Parker and Mateusz Ujma. Permissive Controller Synthesis for Probabilistic Systems. Logical Methods in Computer Science, 11(2). 2015. [pdf] [bib] [Proposes techniques for permissive controller synthesis on stochastic games, implemented in an extension of PRISM.]
[Wil15] Clemens Wiltsche. Assume-Guarantee Strategy Synthesis for Stochastic Games. Ph.D. thesis, Department of Computer Science, University of Oxford. 2015. [pdf] [bib] [Develops strategy synthesis techniques for stochastic games, in particular, compositional methods based on assume-guarantee rules.]
[Ujm15] Mateusz Ujma. On Verification and Controller Synthesis for Probabilistic Systems at Runtime. Ph.D. thesis, Department of Computer Science, University of Oxford. 2015. [pdf] [bib] [Develops various techniques for probabilistic verification and controller synthesis at runtime: incremental model checking, permissive controller synthesis and learning-based controller synthesis.]
[LPH15] Bruno Lacerda, David Parker and Nick Hawes. Optimal Policy Generation for Partially Satisfiable Co-Safe LTL Specifications. In Proc. 24th International Joint Conference on Artificial Intelligence (IJCAI'15), pages 1587-1593, IJCAI/AAAI. August 2015. [pdf] [bib] [Proposes techniques for synthesising optimal policies in MDPs, building on multi-objective probabilistic model checking and PRISM, and applies them to robot task planning.]
[BBDL+15] Tomas Babiak, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Kretinsky, David Muller, David Parker and Jan Strejcek. The Hanoi Omega-Automata Format. In Proc. 27th International Conference on Computer Aided Verification (CAV'15), volume 9206 of LNCS, pages 479-486, Springer. July 2015. [pdf] [bib] [Proposes an exchange format for omega automata, and describes implemented support in a variety of tools, including PRISM.]
[BKTW15] Nicolas Basset, Marta Kwiatkowska, Ufuk Topcu and Clemens Wiltsche. Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives. In Proc. 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15), volume 9035 of LNCS, pages 256-271, Springer. April 2015. [pdf] [bib] [Proposes strategy synthesis for stochastic games with multiple long-run objectives, implemented in an extension of PRISM.]
[DHK14] Frits Dannenberg, Ernst Moritz Hahn and Marta Kwiatkowska. Computing Cumulative Rewards using Fast Adaptive Uniformisation. ACM Transactions on Modeling and Computer Simulation, Special Issue on Computational Methods in Systems Biology. 2014. [pdf] [bib] [Develops fast adaptive uniformisation techniques for cumulative reward properties, implemented in PRISM.]
[BCC+14] Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelík, Vojtěch Forejt, Jan Křetínský, Marta Kwiatkowska, David Parker and Mateusz Ujma. Verification of Markov Decision Processes using Learning Algorithms. In Proc. 12th International Symposium on Automated Technology for Verification and Analysis (ATVA'14), volume 8837 of LNCS, pages 98-114, Springer. November 2014. [pdf] [bib] [Presents MDP verification techniques, implemented in PRISM, based on real-time dynamic programming and delayed Q-learning.]
[CDKP14] Milan Ceska, Frits Dannenberg, Marta Kwiatkowska and Nicola Paoletti. Precise Parameter Synthesis for Stochastic Biochemical Systems. In Proc. 12th International Conference on Computational Methods in Systems Biology (CMSB'14), volume 8859 of LNCS/LNBI, pages 86-98, Springer. November 2014. [pdf] [bib] [Proposes parameter synthesis techniques for CSL properties on stochastic biochemical networks, to implemented in PRISM.]
[BKW14] Nicolas Basset, Marta Kwiatkowska and Clemens Wiltsche. Compositional Controller Synthesis for Stochastic Games. In P. Baldan and D. Gorla (editors), Proc. 25th International Conference on Concurrency Theory (CONCUR'14), volume 8704 of LNCS, pages 173-187, Springer. September 2014. [pdf] [bib] [Proposes compositional assume-guarantee strategy synthesis techniques for stochastic 2-player games.]
[Sim14] Aistis Simaitis. Automatic Verification of Competitive Stochastic Systems. Ph.D. thesis, Department of Computer Science, University of Oxford. March 2014. [pdf] [bib] [Presents novel techniques for verification using stochastic multi-player games and implements them in PRISM-games, an extension of PRISM.]
[KNPQ13] Marta Kwiatkowska, Gethin Norman, David Parker and Hongyang Qu. Compositional Probabilistic Verification through Multi-Objective Model Checking. Information and Computation, 232, pages 38-65, Elsevier. November 2013. [pdf] [bib] [Presents assume-guarantee verification techniques for probabilistic automata, implemented as an extension of PRISM.]
[DHK13] Frits Dannenberg, Ernst Moritz Hahn and Marta Kwiatkowska. Computing Cumulative Rewards using Fast Adaptive Uniformisation. In Proc. 11th International Conference on Computational Methods in Systems Biology (CMSB'13), volume 8130 of LNCS, pages 33-49, Springer. September 2013. [pdf] [bib] [Develops fast adaptive uniformisation techniques for cumulative reward properties, implemented in PRISM.]
[CFK+13c] Taolue Chen, Vojtech Forejt, Marta Kwiatkowska, Aistis Simaitis and Clemens Wiltsche. On Stochastic Games with Multiple Objectives. In Proc. 38th International Symposium on Mathematical Foundations of Computer Science (MFCS'13), volume 8087 of LNCS, pages 266-277, Springer. August 2013. [pdf] [bib] [Studies strategy synthesis and Pareto set approximation for multiple reward objectives in stochastic 2-player games.]
[CFK+13b] Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, David Parker and Aistis Simaitis. Automatic Verification of Competitive Stochastic Systems. Formal Methods in System Design, 43(1), pages 61-92, Springer. August 2013. [pdf] [bib] [Introduces model checking techniques for stochastic multi-player games, implemented in the PRISM-games tool.]
[CKSW13] Taolue Chen, Marta Kwiatkowska, Aistis Simaitis and Clemens Wiltsche. Synthesis for Multi-Objective Stochastic Games: An Application to Autonomous Urban Driving. In Proc. 10th International Conference on Quantitative Evaluation of SysTems (QEST'13), volume 8054 of LNCS, pages 322-337, Springer. August 2013. [pdf] [bib] [Proposes multi-objective strategy synthesis techniques for stochastic games, implemented in PRISM-games, and applies them to an autonomous vehicle case study.]
[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.]
[CFK+12b] Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, Aistis Simaitis, Ashutosh Trivedi and Michael Ummels. Playing Stochastic Games Precisely. In 23rd International Conference on Concurrency Theory (CONCUR'12), volume 7454 of LNCS, pages 348-363, Springer. September 2012. [pdf] [bib] [Proposes model checking techniques for stochastic games against temporal logic properties with precise bounds, as implemented in PRISM-games.]
[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.]
[KNP10b] Marta Kwiatkowska, Gethin Norman and David Parker. A Framework for Verification of Software with Time and Probabilities. In Proc. 8th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'10), volume 6246 of LNCS, pages 25-45, Springer. September 2010. [pdf] [bib] [Extends PRISM's game-based abstraction-refinement methods for PTAs, to real-time probabilistic programs with data.]
[Nim10] Vincent Nimal. Statistical Approaches for Probabilistic Model Checking. MSc Mini-project Dissertation, Oxford University Computing Laboratory. September 2010. [pdf] [bib] [Investigates approximate/statistical model checking techniques and implements them in PRISM.]
[KKNP10] Mark Kattenbelt, Marta Kwiatkowska, Gethin Norman and David Parker. A Game-based Abstraction-Refinement Framework for Markov Decision Processes. Formal Methods in System Design, 36(3), pages 246-280, Springer. September 2010. [pdf] [bib] [Presents game-based abstraction-refinement techniques for MDPs, as used for example to verify PTAs in PRISM.]
[KNP09c] Marta Kwiatkowska, Gethin Norman and David Parker. Stochastic Games for Verification of Probabilistic Timed Automata. In Proc. 7th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'09), volume 5813 of LNCS, pages 212-227, Springer. September 2009. [pdf] [bib] [Presents game-based abstraction-refinement techniques for verifying PTAs, implemented in PRISM.]
[EKVY08] K. Etessami, M. Kwiatkowska, M. Vardi and M. Yannakakis. Multi-Objective Model Checking of Markov Decision Processes. Logical Methods in Computer Science, 4(4), pages 1-21. 2008. [pdf] [bib] http://www.lmcs-online.org/ojs/viewarticle.php?id=364&layout=abstract
[KNSW07] M. Kwiatkowska, G. Norman, J. Sproston and F. Wang. Symbolic Model Checking for Probabilistic Timed Automata. Information and Computation, 205(7), pages 1027-1077. July 2007. [ps.gz] [pdf] [bib]
[EKVY07] K. Etessami, M. Kwiatkowska, M. Vardi and M. Yannakakis. Multi-Objective Model Checking of Markov Decision Processes. In Proc. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), volume 4424 of LNCS, pages 50-65, Springer. March 2007. [pdf] [bib] [Proposes techniques to perform multi-objective model checking of MDPs, later implemented in PRISM.]
[GNB+06] Marcus Groesser, Gethin Norman, Christel Baier, Frank Ciesinski, Marta Kwiatkowska, David Parker. On reduction criteria for probabilistic reward models. In S. Arun-Kumar and N. Garg (editors), Proc. 25th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'06), volume 4337 of Lecture Notes in Computer Science, pages 309-320, Springer Verlag. December 2006. [ps.gz] [pdf] [bib]
[Wan06] F. Wang. Symbolic Implementation of Model-Checking Probabilistic Timed Automata. Ph.D. thesis, University of Birmingham. September 2006. [pdf] [bib]
[KNP06b] Marta Kwiatkowska, Gethin Norman and David Parker. Game-based Abstraction for Markov Decision Processes. In Proc. 3rd International Conference on Quantitative Evaluation of Systems (QEST'06), pages 157-166, IEEE CS Press. Winner of the QEST'06 Best Paper Award. September 2006. [ps.gz] [pdf] [bib]
[KNP06a] Marta Kwiatkowska, Gethin Norman and David Parker. Symmetry Reduction for Probabilistic Model Checking. In T. Ball and R. Jones (editors), Proc. 18th International Conference on Computer Aided Verification (CAV'06), volume 4144 of Lecture Notes in Computer Science, pages 234-248, Springer-Verlag. August 2006. [ps.gz] [pdf] [bib]
[KNPS06] Marta Kwiatkowska, Gethin Norman, David Parker and Jeremy Sproston. Performance Analysis of Probabilistic Timed Automata using Digital Clocks. Formal Methods in System Design, 29, pages 33-78, Springer. August 2006. [ps.gz] [pdf] [bib]
[YKNP06] Håkan Younes, Marta Kwiatkowska, Gethin Norman and David Parker. Numerical vs. Statistical Probabilistic Model Checking. International Journal on Software Tools for Technology Transfer (STTT), 8(3), pages 216-228, Springer. June 2006. [ps.gz] [pdf] [bib]
[ZPK05a] Yi Zhang, David Parker and Marta Kwiatkowska. A Wavefront Parallelisation of CTMC Solution using MTBDDs. In Proc. International Conference on Dependable Systems and Networks (DSN'05), pages 732-742, IEEE CS Press. June 2005. [ps.gz] [pdf] [bib]
[Hin05] A. Hinton. Software Project M60: Simulator for the Probabilistic Model Checker PRISM. MEng Final Year Project Dissertation, School of Computer Science, University of Birmingham. April 2005. [ps.gz] [pdf] [bib]
[Meh04b] R. Mehmood. Disk-based techniques for efficient solution of large Markov chains. Ph.D. thesis, University of Birmingham. October 2004. [ps.gz] [pdf] [bib]
[KNSW04] M. Kwiatkowska, G. Norman, J. Sproston and F. Wang. Symbolic Model Checking for Probabilistic Timed Automata. In Y. Lakhnech and S. Yovine (editors), Proc. FORMATS/FTRTFT'04, volume 3253 of Lecture Notes in Computer Science, pages 293-308, Springer. September 2004. [ps.gz] [pdf] [bib]
[KNP04b] Marta Kwiatkowska, Gethin Norman and David Parker. Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach. International Journal on Software Tools for Technology Transfer (STTT), 6(2), pages 128-142. September 2004. [ps.gz] [pdf] [bib]
[MP04] Andrew Miner and David Parker. Symbolic Representations and Analysis of Large Probabilistic Systems. In C. Baier, B. Haverkort, H. Hermanns, J-P. Katoen, M. Siegle and F. Vaandrager (editors), Validation of Stochastic Systems: A Guide to Current Research, volume 2925 of Lecture Notes in Computer Science, pages 296-338. August 2004. [ps.gz] [pdf] [bib] [Tutorial/survey paper on symbolic methods for probabilistic verification, including the (MD)BDD-based methods in PRISM.]
[YKNP04] Håkan Younes, Marta Kwiatkowska, Gethin Norman and David Parker. Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study. In K. Jensen and A. Podelski (editors), Proc. TACAS'04, volume 2988 of Lecture Notes in Computer Science, pages 46-60, Springer. March 2004. [ps.gz] [pdf] [bib] [Evaluates trade-offs between numerical and statistical approaches to probabilistic model checking using an implementation in PRISM.]
[MPK03b] Rashid Mehmood, David Parker and Marta Kwiatkowska. An Efficient BDD-Based Implementation of Gauss-Seidel for CTMC Analysis. Technical report CSR-03-13, School of Computer Science, University of Birmingham. December 2003. [ps.gz] [pdf] [bib]
[KNS03d] M. Kwiatkowska, G. Norman and J. Sproston. Symbolic Model Checking for Probabilistic Timed Automata. Technical report CSR-03-10, School of Computer Science, University of Birmingham. October 2003. [ps.gz] [pdf] [bib]
[KNPS03] Marta Kwiatkowska, Gethin Norman, David Parker and Jeremy Sproston. Performance Analysis of Probabilistic Timed Automata using Digital Clocks. In Proc. Formal Modeling and Analysis of Timed Systems (FORMATS'03), volume 2791 of LNCS, pages 105-120, Springer. September 2003. [ps.gz] [pdf] [bib]
[MPK03a] Rashid Mehmood, David Parker and Marta Kwiatkowska. An Efficient Symbolic Out-of-Core Solution Method for Markov Models. Technical report CSR-03-08, School of Computer Science, University of Birmingham. August 2003. [ps.gz] [pdf] [bib]
[HKN+03] Holger Hermanns, Marta Kwiatkowska, Gethin Norman, David Parker and Markus Siegle. On the use of MTBDDs for Performability Analysis and Verification of Stochastic Systems. Journal of Logic and Algebraic Programming: Special Issue on Probabilistic Techniques for the Design and Analysis of Systems, 56, pages 23-67, Elsevier. June 2003. [ps.gz] [pdf] [bib]
[Par02] David Parker. Implementation of Symbolic Model Checking for Probabilistic Systems. Ph.D. thesis, University of Birmingham. 2002. [pdf] [bib]
[KNSS02] M. Kwiatkowska, G. Norman, R. Segala and J. Sproston. Automatic Verification of Real-time Systems with Discrete Probability Distributions. Theoretical Computer Science, 282, pages 101-150. June 2002. [ps.gz] [pdf] [bib]
[KNP02b] Marta Kwiatkowska, Gethin Norman and David Parker. Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach. In J-P. Katoen and P. Stevens (editors), Proc. TACAS'02, volume 2280 of Lecture Notes in Computer Science, pages 52-66, Springer. April 2002. [ps.gz] [pdf] [bib] [Introduces the PRISM tool and, in particular, its "hybrid" engine developed to improve the efficiency of symbolic probabilistic model checking.]
[Spr01] J. Sproston. Model Checking for Probabilistic Timed and Hybrid Systems. Ph.D. thesis, School of Computer Science, The University of Birmingham. 2001. [ps] [ps.gz] [bib]
[KKNP01] Joost-Pieter Katoen, Marta Kwiatkowska, Gethin Norman and David Parker. Faster and Symbolic CTMC Model Checking. In L. de Alfaro and S. Gilmore (editors), Proc. PAPM/PROBMIV'01, volume 2165 of Lecture Notes in Computer Science, pages 23-38, Springer. September 2001. [ps.gz] [pdf] [bib]
[KNS01b] M. Kwiatkowska, G. Norman and J. Sproston. Symbolic computation of maximal probabilistic reachability. In K. Larsen and M. Nielsen (editors), Proc. 13th International Conference on Concurrency Theory (CONCUR'01), volume 2154 of LNCS, pages 169-183, Springer. August 2001. [ps.gz] [pdf] [bib]
[KNP00] Marta Kwiatkowska, Gethin Norman and David Parker. Verifying Randomized Distributed Algorithms with PRISM. In Proc. Workshop on Advances in Verification (Wave'2000). July 2000. [ps.gz] [pdf] [bib] [Describes an early version of PRISM and its applicability to analysing randomised distributed algorithms.]
[dAKN+00] Luca de Alfaro, Marta Kwiatkowska, Gethin Norman, David Parker and Roberto Segala. Symbolic Model Checking of Probabilistic Processes using MTBDDs and the Kronecker Representation. In S. Graf and M. Schwartzbach (editors), Proc. TACAS'00, volume 1785 of Lecture Notes in Computer Science, pages 395-410, Springer. March 2000. [ps.gz] [pdf] [bib] [Proposes symbolic techniques for probabilistic model checking and implements them in an early version of PRISM.]

Extensions and adaptions to PRISM (49)

[EPF24] Ingy Elsayed-Aly, David Parker and Lu Feng. Distributional Probabilistic Model Checking. In Proc. 16th NASA Formal Methods Symposium (NFM'24), Springer. To appear. June 2024. [pdf] [bib] [Proposes a probabilistic model checking framework for distributional queries, implemented as an extension of PRISM.]
[SPF24] Shili Sheng, David Parker and Lu Feng. Safe POMDP Online Planning via Shielding. In Proc. IEEE International Conference on Robotics and Automation (ICRA'24). To appear. May 2024. [pdf] [bib] [Presents techniques to augment POMDP online planning with shielding to ensure safety, implemented as an extension of PRISM.]
[Bac22] Edoardo Bacci. Formal Verification of Deep Reinforcement Learning Agents. Ph.D. thesis, School of Computer Science, University of Birmingham. 2022. [pdf] [bib] [Proposes several techniques for verification of deep reinforcement learning policies, with implementations building upon PRISM. ]
[YSD+22] Rui Yan, Gabriel Santos, Xiaoming Duan, David Parker and Marta Kwiatkowska. Finite-horizon Equilibria for Neuro-symbolic Concurrent Stochastic Games. In Proc. 38th Conference on Uncertainty in Artificial Intelligence (UAI'22), Proceedings of Machine Learning Research 180. August 2022. [pdf] [bib] [Develops methods for finite-horizon analysis of neuro-symbolic concurrent stochastic games, implemented on top of PRISM-games.]
[CBPF22] Shenghui Chen, Kayla Boggess, David Parker and Lu Feng. Multi-Objective Controller Synthesis with Uncertain Human Preferences. In Proc. ACM/IEEE 13th International Conference on Cyber-Physical Systems (ICCPS'22), pages 170-180, IEEE. May 2022. [pdf] [bib] [Develops techniques for multi-objective MDP controller synthesis over uncertain preferences, implemented in an extension of PRISM.]
[BAJ+22] Thom S. Badings, Alessandro Abate, Nils Jansen, David Parker, Hasan A. Poonawala and Marielle Stoelinga. Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise. In Proc. 36th AAAI Conference on Artificial Intelligence (AAAI'22), pages 9669-9678. Distinguished Paper Award. March 2022. [pdf] [bib] [Presents methods to synthesise controllers, with probabilistic guarantees obtained using an extension of PRISM for IMDPs.]
[LFPH19] Bruno Lacerda, Fatma Faruq, David Parker and Nick Hawes. Probabilistic Planning with Formal Performance Guarantees for Mobile Service Robots. International Journal of Robotics Research, 38(9), pages 1098–1123. 2019. [pdf] [bib] [Presents a framework for mobile service robot with formal performance guarantees, with an implementation built on PRISM.]
[ELK19] Francisco Eiras, Morteza Lahijanian and Marta Kwiatkowska. Correct-by-Construction Advanced Driver Assistance Systems Based on a Cognitive Architecture. In Proc. IEEE 2nd Connected and Automated Vehicles Symposium (CAVS'19), pages 1-7, IEEE. 2019. [pdf] [bib] [Formally analyses a driver assistance system and a human driver model, with an implementation building on PRISM.]
[EP19] Alexandros Evangelidis and David Parker. Quantitative Verification of Numerical Stability for Kalman Filters. In Proc. 23rd International Symposium on Formal Methods (FM'19), volume 11800 of LNCS, pages 425-441, Springer. October 2019. [pdf] [bib] [Builds a framework for verifying Kalman filters on top of PRISM.]
[NP19] Chris Novakovic and David Parker. Automated Formal Analysis of Side-Channel Attacks on Probabilistic Systems. In Proc. 24th European Symposium on Research in Computer Security (ESORICS'19), volume 11735 of LNCS, pages 319-337, Springer. September 2019. [pdf] [bib] [Develops techniques to identify side-channel attacks in probabilistic systems, building on PRISM-pomdps.]
[PFF+19] Avi Pfeffer, Curt Wu, Gerald Fry, Kenny Lu, Steve Marotta, Mike Reposa, Yuan Shi, T. K. Satish Kumar, Craig A. Knoblock, David Parker, Irfan Muhammad and Chris Novakovic. Software Adaptation for an Unmanned Undersea Vehicle. IEEE Software, 36(2), pages 91-96, IEEE. March 2019. [pdf] [bib] [Summarises the PRINCESS project, which develops methods for adapting an optimising software at runtime, including mission verification using extensions of PRISM.]
[FLHP18] Fatma Faruq, Bruno Lacerda, Nick Hawes and David Parker. Simultaneous Task Allocation and Planning Under Uncertainty. In Proc. IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS'18), IEEE. October 2018. [pdf] [bib] [Proposes techniques for verified multi-robot task allocation and planning, implemented as an extension of PRISM.]
[Kam18] Nishanthan Kamaleson. Model Reduction Techniques for Probabilistic Verification of Markov Chains. Ph.D. thesis, University of Birmingham. April 2018. [pdf] [bib] [Develops several model reduction techniques, for finite-horizon bisimulation and linear inductive models, and implements them in extensions of PRISM.]
[MDPR18] Chunyan Mu, Peter Dittrich, David Parker and Jonathan E. Rowe. Organisation-Oriented Coarse Graining and Refinement of Stochastic Reaction Networks. IEEE/ACM Transactions on Computational Biology and Bioinformatics, 15(4), pages 1152-1166. February 2018. [pdf] [bib] [Presents techniques for analysing chemical reaction networks, based on chemical organisation theory, and implemented as an extension of PRISM.]
[CCGKP17] Radu Calinescu, Milan Češka, Simos Gerasimou, Marta Kwiatkowska and Nicola Paoletti. Designing Robust Software Systems through Parametric Markov Chain Synthesis. In Proc. IEEE International Conference on Software Architecture (ICSA'17), pages 131-140, IEEE Computer Society. 2017. [pdf] [bib] [Synthesises software system designs with a toolchain building on the PRISM extension PRISM-PSY.]
[LPH17] Bruno Lacerda, David Parker and Nick Hawes. Multi-objective Policy Generation for Mobile Robots under Probabilistic Time-Bounded Guarantees. In Proc. 27th International Conference on Automated Planning and Scheduling (ICAPS'17), pages 504-512, AAAI Press. June 2017. [pdf] [bib] [Proposes techniques for generating mobile robot controllers with probabilistic time-bounded guarantees using multi-objective probabilistic model checking and an extension of PRISM.]
[NPZ17] Gethin Norman, David Parker and Xueyi Zou. Verification and Control of Partially Observable Probabilistic Systems. Real-Time Systems, 53(3), pages 354-402, Springer. April 2017. [pdf] [bib] [Presents techniques and a tool for verification and strategy synthesis in partially observable probabilistic models with both discrete and dense models of time.]
[BBBK16] Benoit Barbot, Nicolas Basset, Marc Beunardeau and Marta Kwiatkowska. Uniform Sampling for Timed Automata with Application to Language Inclusion Measurement. In Proc. 13th International Conference on Quantitative Evaluation of SysTems (QEST 2016), volume 9826 of LNCS, pages 175-190, Springer. 2016. [pdf] [bib] [Develops Monte Carlo model checking techniques for timed automata using PRISM, SageMath and COSMOS.]
[MDPR16] Chunyan Mu, Peter Dittrich, David Parker and Jonathan E. Rowe. Formal Quantitative Analysis of Reaction Networks Using Chemical Organisation Theory. In Proc. 14th International Conference on Computational Methods in Systems Biology (CMSB'16), volume 9859 of LNCS, pages 232-251, Springer. September 2016. [pdf] [bib] [Develops techniques for analysing reaction networks using chemical organisation theory, implemented in an extension of PRISM.]
[CPPBK16] Milan Ceska, Petr Pilar, Nicola Paoletti, Lubos Brim and Marta Kwiatkowska. PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems. In Proc. 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16), volume 9636 of LNCS, pages 367–384, Springer. April 2016. [pdf] [bib] [Introduces an extension of PRISM in the form of GPU-accelerated tool for parameter synthesis of stochastic systems. ]
[NPZ15] Gethin Norman, David Parker and Xueyi Zou. Verification and Control of Partially Observable Probabilistic Real-Time Systems. In Proc. 13th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'15), volume 9268 of LNCS, pages 240-255, Springer. September 2015. [pdf] [bib] [Develops techniques for verification and controller synthesis on a partially observable variant of probabilistic timed automata, implemented in an extension of PRISM.]
[LPH14b] Bruno Lacerda, David Parker and Nick Hawes. Optimal and Dynamic Planning for Markov Decision Processes with Co-Safe LTL Specifications. In Proc. IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS'14), pages 1511-1516, IEEE. September 2014. [pdf] [bib] [Proposes a dynamic planning approach for co-safe LTL, implements it in an extension of PRISM and deploys it on a mobile service robot.]
[Gir14] Sergio Giro. Optimal Schedulers vs Optimal Bases: An approach for efficient exact solving of Markov decision processes. Theoretical Computer Science, 538, pages 70–83, Elsevier. June 2014. [pdf] [bib] [Investigates exact-arithmetic model checking methods for MDPs, implemented in an extension of PRISM.]
[DKPQ14] Klaus Draeger, Marta Kwiatkowska, David Parker and Hongyang Qu. Local Abstraction Refinement for Probabilistic Timed Programs. Theoretical Computer Science, 538, pages 37-53, Elsevier. June 2014. [pdf] [bib] [Presents new techniques for abstraction refinement on probabilistic timed programs (probabilistic timed automata with data variables), implemented in an extension of PRISM.]
[AKNP14] Alessandro Abate, Marta Kwiatkowska, Gethin Norman and David Parker. Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations. In F. van Breugel, E. Kashefi, C. Palamidessi and J. Rutten (editors), Horizons of the Mind. A Tribute to Prakash Panangaden, volume 8464 of LNCS, pages 40-58, Springer. May 2014. [pdf] [bib] [Performs probabilistic model checking on continuous-state models using a finite-state abstraction which is then passed to PRISM.]
[DFK+14] Klaus Draeger, Vojtěch Forejt, Marta Kwiatkowska, David Parker and Mateusz Ujma. Permissive Controller Synthesis for Probabilistic Systems. In Proc. 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), volume 8413 of LNCS, pages 531-546, Springer. April 2014. [pdf] [bib] [Presents permissive controller synthesis techniques for stochastic games, implemented in an extension of PRISM.]
[KPQU14] Marta Kwiatkowska, David Parker, Hongyang Qu and Mateusz Ujma. On Incremental Quantitative Verification for Probabilistic Systems. In Andrei Voronkov and Margarita Korovina (editors), HOWARD-60: A Festschrift on the Occasion of Howard Barringer's 60th Birthday, pages 245-257, Easychair. February 2014. [pdf] [bib] http://www.easychair.org/publications/?page=195264436 [Describes incremental methods for runtime probabilistic model checking, implemented in an extension of PRISM.]
[Fen13] Lu Feng. On Learning Assumptions for Compositional Verification of Probabilistic Systems. Ph.D. thesis, University of Oxford. October 2013. [pdf] [bib] [Develops several assume-guarantee techniques for compositional probabilistic verification using automatic generation of assumptions. Implements the techniques using various extensions of PRISM.]
[CHH+13] Taolue Chen, Ernst Moritz Hahn, Tingting Han, Marta Kwiatkowska, Hongyang Qu and Lijun Zhang. Model Repair for Markov Decision Processes. In Proc. 7th International Symposium on Theoretical Aspects of Software Engineering (TASE'13), pages 85--92, IEEE. July 2013. [pdf] [bib] [Proposes approximate solution methods for the problem of model repair on Markov decision processes, implemented as an extension of 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.]
[FKP+12] Vojtěch Forejt, Marta Kwiatkowska, David Parker, Hongyang Qu and Mateusz Ujma. Incremental Runtime Verification of Probabilistic Systems. In Proc. 3rd International Conference on Runtime Verification (RV'12), volume 7686 of LNCS, pages 314-319, Springer. September 2012. [pdf] [bib] [Proposes incremental methods for runtime probabilistic model checking, implemented in an extension of PRISM.]
[Gir12] Sergio Giro. Efficient Computation of Exact Solutions for Quantitative Model Checking. In Proc. 10th Workshop on Quantitative Aspects of Programming Languages (QAPL'12), volume 85 of EPTCS, pages 17-32. March 2012. [pdf] [bib] [Investigates exact-arithmetic model checking methods for MDPs, implemented in an extension of PRISM.]
[HKQ11] Henri Hansen, Marta Kwiatkowska and Hongyang Qu. Partial Order Reduction for Model Checking Markov Decision Processes under Unconditional Fairness. In Proc. 8th International Conference on Quantitative Evaluation of SysTems (QEST'11), pages 203-212, IEEE CS Press. September 2011. [pdf] [bib] [Presents partial-order reduction methods for MDPs, implemented in an extension of PRISM.]
[KPQ11] Marta Kwiatkowska, David Parker and Hongyang Qu. Incremental Quantitative Verification for Markov Decision Processes. In Proc. IEEE/IFIP International Conference on Dependable Systems and Networks (DSN-PDS'11), pages 359-370, IEEE CS Press. June 2011. [pdf] [bib] [Presents incremental verification techniques for MDPs, implemented as an extension of PRISM.]
[FKP11] Lu Feng, Marta Kwiatkowska and David Parker. Automated Learning of Probabilistic Assumptions for Compositional Reasoning. In Proc. 14th International Conference on Fundamental Approaches to Software Engineering (FASE'11), volume 6603 of LNCS, pages 2-17, Springer. Invited paper. March 2011. [pdf] [bib] [Presents a learning-based compositional verification framework, based on an extension of PRISM.]
[FKN+11] Vojtěch Forejt, Marta Kwiatkowska, Gethin Norman, David Parker and Hongyang Qu. Quantitative Multi-Objective Verification for Probabilistic Systems. In Proc. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11), volume 6605 of LNCS, pages 112-127, Springer. March 2011. [pdf] [bib] [Presents multi-objective and assume-guarantee verification techniques for probabilistic automata, implemented as an extension of PRISM.]
[Kat11] Mark Kattenbelt. Automated Quantitative Software Verification. Ph.D. thesis, Oxford University. March 2011. [pdf] [bib] [Thesis on quantitative verification for software, including probabilistic abstraction-refinement methods that use components from GOTO-CC, SATABS and PRISM.]
[FKP10] Lu Feng, Marta Kwiatkowska and David Parker. Compositional Verification of Probabilistic Systems using Learning. In Proc. 7th International Conference on Quantitative Evaluation of Systems (QEST'10), pages 133-142, IEEE CS Press. September 2010. [pdf] [bib] [Presents a learning-based compositional verification framework, based on an extension of PRISM.]
[KNPQ10] Marta Kwiatkowska, Gethin Norman, David Parker and Hongyang Qu. Assume-Guarantee Verification for Probabilistic Systems. In Proc. 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'10), volume 6015 of LNCS, pages 23-37, Springer. March 2010. [pdf] [bib] [Presents assume-guarantee verification techniques for probabilistic automata, implemented as an extension of PRISM.]
[Mai09] V. Maisonneuve. Automatic heuristic-based generation of MTBDD variable orderings for PRISM models. Internship report, ENS Cachan & Oxford University Computing Laboratory. July 2009. [pdf] [bib] [Develops MTBDD variable ordering heuristics, implemented in an extension of PRISM.]
[Kwi09] M. Kwiatkowska. On Quantitative Software Verification. In C. Pasareanu (editor), Proc. 16th International SPIN Workshop, volume 5578 of LNCS, pages 2-3, Springer. Invited contribution. June 2009. [pdf] [bib] [Describes verification techniques for probabilistic C programs, using components from GOTO-CC, SATABS and PRISM.]
[CK09a] V. Issarny, B. Steffen, B. Jonsson, G. Blair, P. Grace, M. Kwiatkowska, R. Calinescu, P. Inverardi, M. Tivoli, A. Bertolino and A. Sabetta. CONNECT Challenges: Towards Emergent Connectors for Eternal Networked Systems. In Proc. 14th IEEE International Conference on Engineering of Complex Computer Systems. Poster. June 2009. [pdf] [bib] [Provides an overview of the CONNECT project, which incorporates extensions of PRISM.]
[KKNP09] Mark Kattenbelt, Marta Kwiatkowska, Gethin Norman and David Parker. Abstraction Refinement for Probabilistic Software. In Proc. 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'09), volume 5403 of Lecture Notes in Computer Science, pages 182-197, Springer. January 2009. [ps.gz] [pdf] [bib] [Develops verification techniques for probabilistic C programs, using components from GOTO-CC, SATABS and PRISM.]
[RPNdA08] Pritam Roy, David Parker, Gethin Norman and Luca de Alfaro. Symbolic Magnifying Lens Abstraction in Markov Decision Processes. In Proc. 5th International Conference on Quantitative Evaluation of Systems (QEST'08), pages 103-112, IEEE CS Press. September 2008. [pdf] [bib] [Presents a symbolic version of magnifying lens abstraction, implemented as an extension of PRISM.]
[KKNP08a] Mark Kattenbelt, Marta Kwiatkowska, Gethin Norman and David Parker. Game-Based Probabilistic Predicate Abstraction in PRISM. In Proc. 6th Workshop on Quantitative Aspects of Programming Languages (QAPL'08), volume 220 (3) of Electronic Notes in Theoretical Computer Science , pages 5-21 , Elsevier. March 2008. [ps.gz] [pdf] [bib] [Develops predicate abstraction techniques for PRISM, using SMT and game-based abstraction.]
[WK05] F. Wang and M. Kwiatkowska. An MTBDD-based implementation of forward reachability for probabilistic timed automata. In Proc. 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA'05), volume 3707 of Lecture Notes in Computer Science, pages 385-399, Springer. October 2005. [ps.gz] [pdf] [bib]
[ZPK05b] Yi Zhang, David Parker and Marta Kwiatkowska. Grid-enabled Probabilistic Model Checking with PRISM. In Proc. 4th All Hands Meeting Workshop (AHM'05). September 2005. [ps.gz] [pdf] [bib]
[KPZM04] Marta Kwiatkowska, David Parker, Yi Zhang and Rashid Mehmood. Dual-Processor Parallelisation of Symbolic Probabilistic Model Checking. In Proc. 12th International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS'04), pages 123-130, IEEE CS Press. October 2004. [ps.gz] [pdf] [bib]
[Meh04a] R. Mehmood. Serial Disk-based Analysis of Large Stochastic Models. In C. Baier, B. Haverkort, H. Hermanns, J-P. Katoen, M. Siegle and F. Vaandrager (editors), Validation of Stochastic Systems: A Guide to Current Research, volume 2925 of Lecture Notes in Computer Science, Springer-Verlag. August 2004. [ps.gz] [pdf] [bib]

Tool/language connections to PRISM (23)

[BRA+23] Thom Badings, Licio Romao, Alessandro Abate, David Parker, Hasan A. Poonawala, Marielle Stoelinga and Nils Jansen. Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions. Journal of Artificial Intelligence Research, 76, pages 341-391. January 2023. [pdf] [bib] [Presents methods to synthesise controllers, with probabilistic guarantees obtained using an extension of PRISM for IMDPs.]
[Far22] Fatma Faruq. Verified Multi-Robot Planning Under Uncertainty. Ph.D. thesis, School of Computer Science, University of Birmingham. 2022. [pdf] [bib] [Develops various methods for synthesising verified multi-robot policies, with an implementation built on top of PRISM. ]
[SSJP22] Marnix Suilen, Thiago D. Simão, Nils Jansen and David Parker. Robust Anytime Learning of Markov Decision Processes. In Proc. 36th Annual Conference on Neural Information Processing Systems (NeurIPS'22). November 2022. [pdf] [bib] [Proposes a robust, anytime approach to learning MDPs, with an implementation building on PRISM's support for IMDPs.]
[SPH+22] Shili Sheng, Erfan Pakdamanian, Kyungtae Han, Ziran Wang, John Lenneman, David Parker and Lu Feng. Planning for Automated Vehicles with Human Trust. ACM Transactions on Cyber-Physical Systems, 6(4), pages 31:1-31:21. September 2022. [pdf] [bib] [Proposes a trust-based route planning approach for automated vehicles, with an implementation that builds upon PRISM's support for POMDPs.]
[BP22] Edoardo Bacci and David Parker. Verified Probabilistic Policies for Deep Reinforcement Learning. In Proc. 14th International Symposium NASA Formal Methods (NFM'22), volume 13260 of LNCS, pages 193-212, Springer. May 2022. [pdf] [bib] [Presents techniques to produce formal guarantees on the safe execution of probabilistic policies for deep reinforcement learning, building on PRISM's model checking engines.]
[EP21] Alexandros Evangelidis and David Parker. Quantitative Verification of Kalman Filters. Formal Aspects of Computing, 33(4-5), pages 669-693, Springer. February 2021. [pdf] [bib] [Builds a framework for quantitative verification of Kalman filters on top of PRISM. ]
[BP20b] Edoardo Bacci and David Parker. Probabilistic Guarantees for Safe Deep Reinforcement Learning. In Proc. 18th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'20), volume 12288 of LNCS, pages 231-248, Springer. September 2020. [pdf] [bib] [Proposes techniques for probabilistic verification of deep reinforcement learning policies, using PRISM as an underlying model checker.]
[Eva20] Alexandros Evangelidis. Verified Control and Estimation for Cloud Computing. Ph.D. thesis, School of Computer Science, University of Birmingham. June 2020. [pdf] [bib] [Proposes techniques and tools for formal analysis of resource control and estimation mechanisms in cloud computing, building on probabilistic model checking and PRISM.]
[LSM+18b] Morteza Lahijanian, María Svorenová, Akshay A. Morye, Brian Yeomans, Dushyant Rao, Ingmar Posner, Paul Newman, Hadas Kress-Gazit and Marta Kwiatkowska. Resource-Performance Trade-off Analysis for Mobile Robots. IEEE Robotics and Automation Letters, 3(3), pages 1840-1847. 2018. [pdf] [bib] [Proposes a framework for analysing resource-performance trade-offs in mobile robotics, using PRISM as an underlying model checker.]
[ANP16] Zaruhi Aslanyan, Flemming Nielson and David Parker. Quantitative Verification and Synthesis of Attack-Defence Scenarios. In Proc. 29th IEEE Computer Security Foundations Symposium (CSF'16), pages 105-119, IEEE. June 2016. [pdf] [bib] [Proposes formal verification techniques for attack-defence scenarios based on model checking of stochastic games and building on the PRISM-games tool.]
[DKP13] Christian Dehnert, Joost-Pieter Katoen and David Parker. SMT-Based Bisimulation Minimisation of Markov Models. In Proc. 14th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'13), volume 7737 of LNCS, pages 28-47, Springer. January 2013. [pdf] [bib] [Presents new SMT-based bisimulation techniques for Markov chains expressed in the PRISM modelling language.]
[CGKM12] Radu Calinescu, Carlo Ghezzi, Marta Kwiatkowska and Raffaela Mirandola. Self-adaptive Software Needs Quantitative Verification at Runtime. Communications of the ACM, 55(9), pages 69-77, ACM. September 2012. [pdf] [bib] [Describes a framework for quantitative runtime verification that incorporates PRISM.]
[FHKP11] Lu Feng, Tingting Han, Marta Kwiatkowska and David Parker. Learning-based Compositional Verification for Synchronous Probabilistic Systems. In Proc. 9th International Symposium on Automated Technology for Verification and Analysis (ATVA'11), volume 6996 of LNCS, pages 511-521, Springer. October 2011. [pdf] [bib] [Presents a learning-based compositional verification framework which uses PRISM for executing individual queries.]
[CGKMT11] Radu Calinescu, Lars Grunske, Marta Kwiatkowska, Raffaela Mirandola and Giordano Tamburrelli. Dynamic QoS Management and Optimisation in Service-Based Systems. IEEE Transactions on Software Engineering, 37(3), pages 387-409. May 2011. [bib] [Presents a framework for developing adaptive service-based systems, using PRISM to compute QoS properties.]
[CK10] Radu Calinescu and Marta Kwiatkowska. Software Engineering Techniques for the Development of Systems of Systems. In Christine Choppy and Oleg Sokolsky (editors), Proc. 15th Monterey Workshop on Foundations of Computer Software. Future Trends and Techniques for Development (Monterey'08), volume 6028 of LNCS, pages 59-82, Springer. September 2010. [pdf] [bib] http://www.springerlink.com/content/6334127431456134/ [Presents a framework for system-of-systems development, incorporating PRISM.]
[DMP09] Alastair Donaldson, Alice Miller and David Parker. Language-level Symmetry Reduction for Probabilistic Model Checking. In Proc. 6th International Conference on Quantitative Evaluation of Systems (QEST'09), pages 289-298, IEEE Computer Society. September 2009. [pdf] [bib] [Presents symmetry reduction techniques based on translation of PRISM models.]
[CK09] R. Calinescu and M. Kwiatkowska. Using Quantitative Analysis to Implement Autonomic IT Systems. In Proc. 31st International Conference on Software Engineering (ICSE'09), pages 100-110, IEEE Press. May 2009. [pdf] [bib] [Presents an autonomic software framework, incorporating quantitative analysis of system models using PRISM.]
[NPPW09] Gethin Norman, Catuscia Palamidessi, David Parker and Peng Wu. Model Checking Probabilistic and Stochastic Extensions of the Pi-Calculus. IEEE Transactions on Software Engineering, 35(2), pages 209-223, IEEE Computer Society. March 2009. [pdf] [bib] [Presents model checking techniques for the probabilistic/stochastic pi-calculus based on a translation to PRISM.]
[CK09b] R. Calinescu and M. Kwiatkowska. CADS*: Computer-Aided Development of Self-* Systems. In Marsha Chechik and Martin Wirsing (editors), Fundamental Approaches to Software Engineering (FASE 2009), volume 5503 of Lecture Notes in Computer Science, pages 421-424, Springer-Verlag. March 2009. [pdf] [bib] [Presents a tool for developing self-* systems, based on Markov chain analysis using PRISM.]
[CBGP08] Frank Ciesinski, Christel Baier, Marcus Groesser and David Parker. Generating Compact MTBDD-Representations from Probmela Specifications. In Proc. 15th International SPIN Workshop on Model Checking of Software (SPIN'08), volume 5156 of Lecture Notes in Computer Science, pages 60-76, Springer. August 2008. [pdf] [bib] [Presents techniques for efficient translation of Probmela models into the PRISM modelling language.]
[DMP07] Alastair Donaldson, Alice Miller and David Parker. GRIP: Generic Representatives in PRISM. In Proc. 4th International Conference on Quantitative Evaluation of Systems (QEST'07), pages 115-116, IEEE CS Press. September 2007. [ps.gz] [pdf] [bib] [Presents GRIP, a symmetry reduction tool for PRISM models.]
[NPPW07] Gethin Norman, Catuscia Palamidessi, David Parker and Peng Wu. Model Checking the Probabilistic Pi-calculus. In Proc. 4th International Conference on Quantitative Evaluation of Systems (QEST'07), pages 169-178, IEEE CS Press. September 2007. [ps.gz] [pdf] [bib] [Presents model checking techniques for the probabilistic pi-calculus based on a translation to PRISM.]
[FMM07] A. Fehnker, M. Fruth and A. McIver. Graphical modelling for simulation and formal analysis of wireless network protocols. In Proc. Workshop on Methods, Models and Tools for Fault-Tolerance (MeMoT'07) at the 7th International Conference on Integrated Formal Methods (IFM'07), pages 80-87. Technical Report CS-TR-1032, University of Newcastle upon Tyne. July 2007. [pdf] [bib]

Case studies using PRISM (55)

[OPR20] Michael Oxford, David Parker and Mark Ryan. Quantitative Verification of Certificate Transparency Gossip Protocols. In Proc. 6th International Workshop on Security and Privacy in the Cloud (SPC'20), IEEE. June 2020. [pdf] [bib] [Analyses the effectiveness of certificate transparency gossiping protocols using probabilistic model checking and PRISM.]
[FGH+20] Douglas Fraser, Ruben Giaquinta, Ruth Hoffmann, Murray Ireland, Alice Miller and Gethin Norman. Collaborative Models for Autonomous Systems Controller Synthesis. Formal Aspects of Computing, 32, pages 157-186. April 2020. [pdf] [bib] [Synthesises controllers for unmanned aerial vehicles using probabilistic model checking and PRISM.]
[HMP+19] Richard Henze, Chunyan Mu, Mate Puljiz, Nishanthan Kamaleson, Jan Huwald, John Haslegrave, Pietro Speroni di Fenizio, David Parker, Christopher Good, Jonathan E. Rowe, Bashar Ibrahim and Peter Dittrich. Multi-scale Stochastic Organization-oriented Coarse-graining Exemplified on the Human Mitotic Checkpoint. Scientific Reports, 9(1), pages 3902, Nature Research. March 2019. [pdf] [bib] [Analyses biological models at various levels of coarse graining with several different tools, including PRISM.]
[EPB18] Alexandros Evangelidis, David Parker and Rami Bahsoon. Performance Modelling and Verification of Cloud-based Auto-Scaling Policies. Future Generation Computer Systems, 87, pages 629-638, Elsevier. October 2018. [pdf] [bib] [Presents an approach for producing formal performance guarantees for cloud-based auto-scaling policies using PRISM.]
[GHI+18] Ruben Giaquinta, Ruth Hoffmann, Murray Ireland, Alice Miller and Gethin Norman. Strategy Synthesis for Autonomous Agents using PRISM. In Proc. 10th NASA Formal Methods Symposium (NFM 2018), volume 10811 of LNCS, pages 220-236, Springer. March 2018. [pdf] [bib] [Synthesises controllers for unmanned aerial vehicles using probabilistic model checking and PRISM.]
[IK17] Azlan Ismail and Marta Kwiatkowska. Synthesizing Pareto Optimal Decision for Autonomic Clouds using Stochastic Games Model Checking. In Proc. 24th Asia-Pacific Software Engineering Conference (APSEC'17), pages 436-445, IEEE. 2017. [pdf] [bib] [Proposes a multi-objective adaptive decision-making approach for autonomic clouds based on PRISM-games.]
[EPB17] Alexandros Evangelidis, David Parker and Rami Bahsoon. Performance Modelling and Verification of Cloud-based Auto-Scaling Policies. In Proc. IEEE/ACM 17th International Symposium on Cluster, Cloud and Grid Computing (CCGrid'17), pages 355-364, IEEE. May 2017. [pdf] [bib] [Presents an approach for producing formal performance guarantees for cloud-based auto-scaling policies using PRISM.]
[LK16] Morteza Lahijanian and Marta Kwiatkowska. Specification Revision for Markov Decision Processes with Optimal Trade-off. In Proc. 55th Conference on Decision and Control (CDC'16), pages 7411-7418. 2016. [pdf] [bib] [Presents techniques for techniques for analysing trade-offs between the probability of satisfying a specification and the cost of revising, using PRISM as an underlying multi-objective model checker.]
[FWHT16] Lu Feng, Clemens Wiltsche, Laura Humphrey and Ufuk Topcu. Synthesis of Human-in-the-Loop Control Protocols for Autonomous Systems. IEEE Transactions on Automation Science and Engineering, 13(2), pages 450-462. 2016. [bib] [Uses PRISM and PRISM-games to synthesize control protocols for autonomous systems interacting with human operators.]
[HIM+16] Ruth Hoffmann, Murray L. Ireland, Alice Miller, Gethin Norman and Sandor M. Veres. Autonomous Agent Behaviour Modelled in PRISM - A Case Study. In Proc. 23rd International Symposium on Model Checking Software (SPIN'16), pages 104-110. 2016. [Describes the modelling and verification of an unmanned aerial vehicle (UAV) using PRISM.]
[FWHT15] Lu Feng, Clemens Wiltsche, Laura Humphrey and Ufuk Topcu. Controller Synthesis for Autonomous Systems Interacting with Human Operators. In Proc. International Conference on Cyber-Physical Systems (ICCPS'15), ACM. 2015. [pdf] [Uses PRISM and PRISM-games to synthesize control protocols for autonomous systems interacting with human operators.]
[BK15] Benoit Barbot and Marta Kwiatkowska. On Quantitative Modelling and Verification of DNA Walker Circuits Using Stochastic Petri Nets. In Proc. 36th International Conference on Application and Theory of Petri Nets and Concurrency. 2015. [pdf] [Uses probabilistic model checking and PRISM to analyse DNA molecular walkers modelled as stochastic Petri nets.]
[DKTT14] Frits Dannenberg, Marta Kwiatkowska, Chris Thachuk and Andrew J. Turberfield. DNA walker circuits: Computational potential, design, and verification. Natural Computing. 2014. [pdf] [bib] [Designs a discrete stochastic model of DNA walker circuits and analyses it with probabilistic model checking and PRISM.]
[DKTT13] Frits Dannenberg, Marta Kwiatkowska, Chris Thachuk and Andrew J. Turberfield. DNA walker circuits: computational potential, design, and verification. In Proc. 19th International Conference on DNA Computing and Molecular Programming (DNA 19), volume 8141 of LNCS, pages 31-45, Springer. September 2013. [pdf] [bib] [Investigates the reliability, performance and correctness of DNA walker circuits using probabilistic model checking and PRISM.]
[KPS13] Marta Kwiatkowska, David Parker and Aistis Simaitis. Strategic Analysis of Trust Models for User-Centric Networks. In Proc. 1st International Workshop on Strategic Reasoning (SR'13), volume 112 of EPTCS, pages 53-60. March 2013. [pdf] [bib] [Analyses a cooperation model for user-centric networks using PRISM-games.]
[DKN+13] Marie Duflot, Marta Kwiatkowska, Gethin Norman, David Parker, Sylvain Peyronnet, Claudine Picaronny and Jeremy Sproston. Practical Applications of Probabilistic Model Checking to Communication Protocols. In S. Gnesi and T. Margaria (editors), Formal Methods for Industrial Critical Systems: A Survey of Applications, pages 133-150, IEEE Computer Society Press. March 2013. [pdf] [bib] [Applies PRISM and APMC to analyse the IEEE 802.3 (CSMA/CD) protocol.]
[GHK+12] Lucia Gallina, Tingting Han, Marta Kwiatkowska, Andrea Marin, Sabina Rossi and Alvise Spanò. Automatic Energy-aware Performance Analysis of Mobile Ad-hoc Networks. In Proc. 2012 IFIP Wireless Days conference (WD'12). 2012. [pdf] [Presents a framework for analysing the performance of Mobile Ad-hoc Networks (MANETs) using probabilistic process calculi and PRISM.]
[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.]
[KNP12a] Marta Kwiatkowska, Gethin Norman and David Parker. Probabilistic Verification of Herman’s Self-Stabilisation Algorithm. Formal Aspects of Computing, 24(4), pages 661-670, Springer. July 2012. [pdf] [bib] [Analyses Herman's self stabilisation protocol using PRISM.]
[BN12] Péter Biró and Gethin Norman. Analysis of Stochastic Matching Markets. In Proc. 3rd Workshop on Cooperative Games in Multiagent Systems (CoopMAS'12). June 2012. [pdf] [Studies "Stable Matching" problems, including a DTMC-based analysis using PRISM.]
[Fru11] Matthias Fruth. Formal Methods for the Analysis of Wireless Network Protocols. Ph.D. thesis, Oxford University. October 2011. [pdf] [bib] [Analyses wireless network protocols such as Zigbee using probabilistic model checking and PRISM.]
[CKPS11] Taolue Chen, Marta Kwiatkowska, David Parker and Aistis Simaitis. Verifying Team Formation Protocols with Probabilistic Model Checking. In Proc. 12th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA XII 2011), volume 6814 of LNCS, pages 190-297, Springer. July 2011. [pdf] [bib] [Analyses a team formation protocol using PRISM and a prototype extension for stochastic games.]
[YNN+11] Ender Yüksel‚ Hanne Riis Nielson‚ Flemming Nielson‚ Matthias Fruth and Marta Kwiatkowska. Optimizing Key Updates in Sensor Networks. In Proc. IEEE Sensors Applications Symposium (SAS'11), pages 82-87. February 2011. [bib] [Analyses the performance of ZigBee security key updates using PRISM.]
[GKMMQ10] Felicita Di Giandomenico, Marta Kwiatkowska, Marco Martinucci, Paolo Masci, and Hongyang Qu. Dependability Analysis and Verification for Connected Systems. In Tiziana Margaria and Bernhard Steffen (editors), 4th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'10), volume 6416 of LNCS, pages 263-277, Springer. October 2010. [pdf] [Describes a framework for analsyis of connected systems, including probabilistic model checking using PRISM.]
[KH09b] M. Kwiatkowska and J. Heath. Biological pathways as communicating computer systems. Journal of Cell Science, 122(16), pages 2793-2800. August 2009. [bib] http://jcs.biologists.org/cgi/content/abstract/122/16/2793 [Describes the application of various computational tools, including PRISM, to systems biology.]
[KNPV09] Marta Kwiatkowska, Gethin Norman, David Parker and Maria Grazia Vigliotti. Probabilistic Mobile Ambients. Theoretical Computer Science, 410(12-13), pages 1272-1303, Elsevier. March 2009. [ps.gz] [pdf] [bib] [Presents a probabilistic version of the Mobile Ambients calculus and an accompanying case study using PRISM.]
[Ma08] Zhongdan Ma. Modelling with PRISM of Intelligent System. Masters thesis, University of Oxford. 2008. [pdf] [bib] [Uses PRISM to analyse the hand washing problem, in the context of intelligent systems to assist people with dementia.]
[KNP08d] Marta Kwiatkowska, Gethin Norman and David Parker. Analysis of a Gossip Protocol in PRISM. ACM SIGMETRICS Performance Evaluation Review, 36(3), pages 17-22. December 2008. [pdf] [bib] [Analyses a gossip protocol for information dissemination using PRISM.]
[HKN+08] John Heath, Marta Kwiatkowska, Gethin Norman, David Parker and Oksana Tymchyshyn. Probabilistic Model Checking of Complex Biological Pathways. Theoretical Computer Science (Special Issue on Converging Sciences: Informatics and Biology), 391(3), pages 239-257, Elsevier. February 2008. [ps.gz] [pdf] [bib] [Analyses the FGF (Fibroblast Growth Factor) signalling pathway using PRISM.]
[Sch08] O. Schaeffer. On the use of process algebra techniques in computational modelling of cancer initiation and development. Ph.D. thesis, University of Birmingham. February 2008. [pdf] [bib] [Thesis developing computational models of the FGF and Wnt pathways, including the use of PRISM.]
[KNP07b] Marta Kwiatkowska, Gethin Norman and David Parker. Controller Dependability Analysis By Probabilistic Model Checking. Control Engineering Practice, 15(11), pages 1427-1434, Elsevier. November 2007. [ps.gz] [pdf] [bib] [Illustrates the applicability of probabilistic model checking and PRISM to analysing dependability properties for a simple model of a software-based control systems.]
[NS06] G. Norman and V. Shmatikov. Analysis of Probabilistic Contract Signing. Journal of Computer Security, 14(6), pages 561-589, IOS Press. November 2006. [ps.gz] [pdf] [bib] [Analyses several fair exchange and contract signing protocols using PRISM.]
[Fru06] M. Fruth. Probabilistic Model Checking of Contention Resolution in the IEEE 802.15.4 Low-Rate Wireless Personal Area Network Protocol. In Proc. 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'06). November 2006. [pdf] [bib]
[DKNP06] Marie Duflot, Marta Kwiatkowska, Gethin Norman and David Parker. A Formal Analysis of Bluetooth Device Discovery. International Journal on Software Tools for Technology Transfer (STTT), 8(6), pages 621 - 632, Springer-Verlag. November 2006. [ps.gz] [pdf] [bib] [Analyses device discovery in Bluetooth using PRISM.]
[HKN+06] John Heath, Marta Kwiatkowska, Gethin Norman, David Parker and Oksana Tymchyshyn. Probabilistic model checking of complex biological pathways. In C. Priami (editor), Proc. Computational Methods in Systems Biology (CMSB'06), volume 4210 of Lecture Notes in Bioinformatics, pages 32-47, Springer Verlag. October 2006. [ps.gz] [pdf] [bib] [Analyses the FGF (Fibroblast Growth Factor) signalling pathway using PRISM.]
[NPKS05] Gethin Norman, David Parker, Marta Kwiatkowska and Sandeep Shukla. Evaluating the Reliability of NAND Multiplexing with PRISM. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 24(10), pages 1629-1637. October 2005. [ps.gz] [pdf] [bib] [Analyses the reliability of defect-tolerant design, NAND multiplexing, using PRISM.]
[KNP05c] Marta Kwiatkowska, Gethin Norman and David Parker. Probabilistic Model Checking and Power-Aware Computing. In In Proc. 7th International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS), pages 6-9. September 2005. [ps.gz] [pdf] [bib] [Applies PRISM to the analysis of power-aware systems: dynamic power management and dynamic voltage scaling.]
[NPK+05] Gethin Norman, David Parker, Marta Kwiatkowska, Sandeep Shukla and Rajeev Gupta. Using Probabilistic Model Checking for Dynamic Power Management. Formal Aspects of Computing, 17(2), pages 160-176, Springer-Verlag. August 2005. [ps.gz] [pdf] [bib] [Analyses probabilistic dynamic power management (DPM) strategies using PRISM.]
[KNP05d] Marta Kwiatkowska, Gethin Norman and David Parker. Quantitative Analysis with the Probabilistic Model Checker PRISM. Electronic Notes in Theoretical Computer Science, 153(2), pages 5-31, Elsevier. May 2005. [ps.gz] [pdf] [bib] [Gives an overview of PRISM and describes a selection of case studies.]
[KNP05b] Marta Kwiatkowska, Gethin Norman and David Parker. Probabilistic Model Checking in Practice: Case Studies with PRISM. ACM SIGMETRICS Performance Evaluation Review, 32(4), pages 16-21. March 2005. [ps.gz] [pdf] [bib] [Surveys a selection of case studies that have been carried out using PRISM.]
[DKNP04] Marie Duflot, Marta Kwiatkowska, Gethin Norman and David Parker. A Formal Analysis of Bluetooth Device Discovery. In T. Margaria and B. Steffen, A. Philippou and M. Reitenspiess (editors), Proc. 1st International Symposium on Leveraging Applications of Formal Methods (ISOLA'04), volume TR-2004-6 of Technical Report, pages 268-275, Department of Computer Science, University of Cyprus. November 2004. [ps.gz] [pdf] [bib] [Analyses device discovery in Bluetooth using PRISM.]
[Nor04] G. Norman. Analysing Randomized Distributed Algorithms. In C. Baier, B. Haverkort, H. Hermanns, J-P. Katoen, M. Siegle and F. Vaandrager (editors), Validation of Stochastic Systems: A Guide to Current Research, volume 2925 of Lecture Notes in Computer Science, pages 384--418, Springer. October 2004. [ps.gz] [pdf] [bib] [Describes techniques to verify randomised distributed algorithms, including various PRISM-based case studies.]
[DFH+04] M. Duflot, L. Fribourg, T. Hérault, R. Lassaigne, F. Magniette, S. Messika, S. Peyronnet and C. Picaronny. Probabilistic model checking of the CSMA/CD protocol using PRISM and APMC. In Proc. 4th Workshop on Automated Verification of Critical Systems (AVoCS'04), volume 128(6) of Electronic Notes in Theoretical Computer Science, pages 195-214, Elsevier Science. September 2004. [ps.gz] [pdf] [bib]
[KNP04c] Marta Kwiatkowska, Gethin Norman and David Parker. Controller Dependability Analysis By Probabilistic Model Checking. In Proc. 11th IFAC Symposium on Information Control Problems in Manufacturing (INCOM'04), pages 177-182, Elsevier. April 2004. [ps.gz] [pdf] [bib] [Illustrates the applicability of probabilistic model checking and PRISM to analysing dependability properties for a simple model of a software-based control systems.]
[DKN04] C. Daws, M. Kwiatkowska and G. Norman. Automatic Verification of the IEEE 1394 Root Contention Protocol with KRONOS and PRISM. International Journal on Software Tools for Technology Transfer (STTT), 5(2), pages 221-236. March 2004. [ps.gz] [pdf] [bib]
[NPKS04] Gethin Norman, David Parker, Marta Kwiatkowska and Sandeep Shukla. Evaluating the Reliability of Defect-Tolerant Architectures for Nanotechnology with Probabilistic Model Checking. In Proc. International Conference on VLSI Design, pages 907-914, IEEE CS Press. January 2004. [ps.gz] [pdf] [bib] [Analyses the reliability of defect-tolerant design, NAND multiplexing, using PRISM.]
[NPK+03] Gethin Norman, David Parker, Marta Kwiatkowska, Sandeep Shukla and Rajeev Gupta. Using Probabilistic Model Checking for Dynamic Power Management. In Proc. 3rd Workshop on Automated Verification of Critical Systems (AVoCS'03). Technical Report DSSE-TR-2003-2, University of Southampton. April 2003. [ps.gz] [pdf] [bib] [Analyses probabilistic dynamic power management (DPM) strategies using PRISM.]
[KNS03b] M. Kwiatkowska, G. Norman and J. Sproston. Probabilistic Model Checking of Deadline Properties in the IEEE1394 FireWire Root Contention Protocol. Formal Aspects of Computing, 14(3), pages 295-318. April 2003. [ps.gz] [pdf] [bib]
[NS02] G. Norman and V. Shmatikov. Analysis of Probabilistic Contract Signing. In A. Abdallah, P. Ryan and S. Schneider (editors), Proc. BCS-FACS Formal Aspects of Security (FASec'02), volume 2629 of Lecture Notes in Computer Science, pages 81-96, Springer. December 2002. [ps.gz] [pdf] [bib]
[KN02] M. Kwiatkowska and G. Norman. Verifying Randomized Byzantine Agreement. In D. Peled and M. Vardi (editors), Proc. Formal Techniques for Networked and Distributed Systems (FORTE'02), volume 2529 of Lecture Notes in Computer Science, pages 194-209, Springer. November 2002. [ps.gz] [pdf] [bib]
[NPK+02] Gethin Norman, David Parker, Marta Kwiatkowska, Sandeep Shukla and Rajeev Gupta. Formal Analysis and Validation of Continuous Time Markov Chain Based System Level Power Management Strategies. In Proc. 7th Annual IEEE International Workshop on High Level Design Validation and Test (HLDVT'02), pages 45-50, OmniPress. October 2002. [ps.gz] [pdf] [bib] [Analyses probabilistic dynamic power management (DPM) strategies using CTMC models built with PRISM.]
[DKN02] C. Daws, M. Kwiatkowska and G. Norman. Automatic Verification of the IEEE 1394 Root Contention Protocol with KRONOS and PRISM. In Proc. 7th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'02), volume 66.2 of ENTCS. July 2002. [ps.gz] [pdf] [bib]
[KNS02a] M. Kwiatkowska, G. Norman and J. Sproston. Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol. In H. Hermanns and R. Segala (editors), Proc. PAPM/PROBMIV'02, volume 2399 of Lecture Notes in Computer Science, pages 169-187, Springer. July 2002. [ps.gz] [pdf] [bib]
[KNS01a] M. Kwiatkowska, G. Norman and R. Segala. Automated Verification of a Randomised Distributed Consensus Protocol Using Cadence SMV and PRISM. In G. Berry, H. Common and A. Finkel (editors), Proc. CAV'01, volume 2102 of Lecture Notes in Computer Science, pages 194-206, Springer. January 2001. [ps.gz] [pdf] [bib] [Analyses Aspnes and Herlihy's randomised consensus protocol using PRISM and Cadence SMV.]

PRISM tool papers (9)

[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.]
[KPW18] Marta Kwiatkowska, David Parker and Clemens Wiltsche. PRISM-games: Verification and Strategy Synthesis for Stochastic Multi-player Games with Multiple Objectives. International Journal on Software Tools for Technology Transfer, 20(2), pages 195–210, Springer. April 2018. [pdf] [bib] [Provides a detailed overview of PRISM-games, including its modelling and property specification formalisms, underlying architecture and implementation, experimental results and case studies.]
[KPW16] Marta Kwiatkowska, David Parker and Clemens Wiltsche. PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games. In Proc. 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16), volume 9636 of LNCS, pages 560-566, Springer. April 2016. [pdf] [bib] [Introduces version 2.0 of the PRISM-games tool.]
[CFK+13] Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, David Parker and Aistis Simaitis. PRISM-games: A Model Checker for Stochastic Multi-Player Games. In Proc. 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13), volume 7795 of LNCS, pages 185-191, Springer. March 2013. [pdf] [bib] [Introduces PRISM-games, a model checker for stochastic multi-player games.]
[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.]
[HKNP06] Andrew Hinton, Marta Kwiatkowska, Gethin Norman and David Parker. PRISM: A Tool for Automatic Verification of Probabilistic Systems. In H. Hermanns and J. Palsberg (editors), Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06), volume 3920 of Lecture Notes in Computer Science, pages 441-444, Springer. March 2006. [ps.gz] [pdf] [bib] [Tool paper describing PRISM.]
[KNP04d] Marta Kwiatkowska, Gethin Norman and David Parker. PRISM 2.0: A Tool for Probabilistic Model Checking. In Proc. 1st International Conference on Quantitative Evaluation of Systems (QEST'04), pages 322-323, IEEE CS Press. September 2004. [ps.gz] [pdf] [bib] [Tool paper describing PRISM 2.0.]
[KNP02a] Marta Kwiatkowska, Gethin Norman and David Parker. PRISM: Probabilistic Symbolic Model Checker. In T. Field, P. Harrison, J. Bradley and U. Harder (editors), Proc. TOOLS 2002, volume 2324 of Lecture Notes in Computer Science, pages 200-204, Springer. April 2002. [ps.gz] [pdf] [bib] [Tool paper describing PRISM.]
[KNP01] Marta Kwiatkowska, Gethin Norman and David Parker. PRISM: Probabilistic Symbolic Model Checker. In Proc. PAPM/PROBMIV'01 Tools Session, pages 7-12. Available as Technical Report 760/2001, University of Dortmund. September 2001. [ps.gz] [pdf] [bib] [Tool paper describing PRISM.]

PRISM-related tutorials and surveys (26)

[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.]
[KNP+22] Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos and Rui Yan. Probabilistic Model Checking for Strategic Equilibria-based Decision Making: Advances and Challenges. In Proc. 47th International Symposium on Mathematical Foundations of Computer Science (MFCS'22), pages 4:1-4:22. August 2022. [pdf] [bib] [Provides an overview of recent work developing a modelling and verification framework using concurrent stochastic games.]
[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.]
[SK16] Maria Svorenova and Marta Kwiatkowska. Quantitative Verification and Strategy Synthesis for Stochastic Games. European Journal of Control, 30, pages 15-30, Elsevier. 2016. [pdf] [bib] [Provides an overview of techniques for quantitative verification and strategy synthesis for stochastic games.]
[Kwi16] Marta Kwiatkowska. Model Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice. In Proc. 43rd International Colloquium on Automata, Languages, and Programming (ICALP'16), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. 2016. [pdf] [bib] [Gives an overview of quantitative verification and strategy synthesis for stochastic multi-player games, as implemented in PRISM-games.]
[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.]
[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.]
[Kwi13] Marta Kwiatkowska. From Software Verification to 'Everyware' Verification. Computer Science - Research and Development, 28(4), pages 295-310, Springer. November 2013. [pdf] [bib] [Summarises ongoing research into verification of 'everyware', including techniques and tools that improve, extend and connect to PRISM.]
[KP13] Marta Kwiatkowska and David Parker. Automated Verification and Strategy Synthesis for Probabilistic Systems. In Proc. 11th International Symposium on Automated Technology for Verification and Analysis (ATVA'13), volume 8172 of LNCS, pages 5-22, Springer. October 2013. [pdf] [bib] [Provides an overview of strategy synthesis techniques for probabilistic models.]
[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.]
[Kwi13b] Marta Kwiatkowska. Advances in Quantitative Verification for Ubiquitous Computing. In Proc. 10th International Colloquium on Theoretical Aspects of Computing (ICTAC'13), volume 8049 of LNCS, pages 42-58, Springer. September 2013. [pdf] [bib] [Invited paper on recent developments in quantitative verification for ubiquitous computing, illustrated by three PRISM case studies. ]
[Kwi12] Marta Kwiatkowska. Sensing Everywhere: Towards Safer and More Reliable Sensor-enabled Devices. In Proc. 31st International Conference on Computer Safety, Reliability and Security (SAFECOMP'12), Springer. September 2012. [pdf] [bib] [Invited talk on research directions for verification of sensor-enabled devices, including PRISM-based analyses.]
[KP12] Marta Kwiatkowska and David Parker. Advances in Probabilistic Model Checking. In Software Safety and Security - Tools for Analysis and Verification, volume 33 of NATO Science for Peace and Security Series - D: Information and Communication Security, pages 126-151, IOS Press. June 2012. [pdf] [bib] [Tutorial paper on probabilistic model checking, covering DTMCs, MDPs, quantitative abstraction refinement, PTAs 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.]
[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.]
[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.]
[KNP09b] Marta Kwiatkowska, Gethin Norman and David Parker. Quantitative Verification Techniques for Biological Processes. In A. Condon, D. Harel, J. Kok, A. Salomaa and E. Winfree (editors), Algorithmic Bioprocesses, pages 391-409, Springer. August 2009. [pdf] [bib] [Tutorial paper on the application of probabilistic model checking and PRISM to biological systems, including an illustrative case study (MAPK cascade).]
[KNP09a] Marta Kwiatkowska, Gethin Norman and David Parker. PRISM: Probabilistic Model Checking for Performance and Reliability Analysis. ACM SIGMETRICS Performance Evaluation Review, 36(4), pages 40-45, ACM. March 2009. [pdf] [bib] [Provides an overview of PRISM and its application to performance and and reliability analysis.]
[KNP08a] Marta Kwiatkowska, Gethin Norman and David Parker. Using Probabilistic Model Checking in Systems Biology. ACM SIGMETRICS Performance Evaluation Review, 35(4), pages 14-21, Association for Computing Machinery. March 2008. [ps.gz] [pdf] [bib] [Illustrates the applicability of PRISM to systems biology, using a case study: the MAPK cascade.]
[KNPS08] Marta Kwiatkowska, Gethin Norman, David Parker and Jeremy Sproston. Verification of Real-Time Probabilistic Systems. In S. Merz and N. Navet (editors), Modeling and Verification of Real-Time Systems: Formalisms and Software Tools, pages 249-288, John Wiley & Sons. January 2008. [pdf] [bib] http://www.iste.co.uk/index.php?p=a&ACTION=View&id=195 [Tutorial on probabilistic timed automata (PTAs) and the methods used by PRISM to analyse them.]
[Kwi07] M. Kwiatkowska. Quantitative Verification: Models, Techniques and Tools. In Proc. 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), pages 449-458, ACM Press. September 2007. [pdf] [bib] [Overview of probabilistic model checking and PRISM, with a particular emphasis on DTMCs.]
[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.]
[KNP+06] Marta Kwiatkowska, Gethin Norman, David Parker, Oksana Tymchyshyn, John Heath and Eamonn Gaffney. Simulation and Verification for Computational Modelling of Signalling Pathways. In Proc. 2006 Winter Simulation Conference, pages 1666-1674. December 2006. [ps.gz] [pdf] [bib] [Surveys techniques for the analysis of cell signalling pathways, including the simulation and model checking techniques in PRISM.]
[KNP04a] Jan Rutten, Marta Kwiatkowska, Gethin Norman and David Parker. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. Volume 23 of CRM Monograph Series. American Mathematical Society. P. Panangaden and F. van Breugel (eds.). March 2004. [bib]
[Kwi03] M. Kwiatkowska. Model Checking for Probability and Time: From Theory to Practice. In Proc. 18th IEEE Symposium on Logic in Computer Science (LICS'03), pages 351-360, IEEE CS Press. Invited paper. June 2003. [ps.gz] [pdf] [bib]

Others

[ABB+24] Roman Andriushchenko, Alexander Bork, Carlos E. Budde, Milan Češka, Kush Grover, Ernst Moritz Hahn, Arnd Hartmanns, Bryant Israelsen, Nils Jansen, Joshua Jeppson, Sebastian Junges, Maximilian A. Köhl, Bettina Könighofer, Jan Křetínský, Tobias Meggendorfer, David Parker, Stefan Pranger, Tim Quatmann, Enno Ruijters, Landon Taylor, Matthias Volk, Maximilian Weininger and Zhen Zhang. Tools at the Frontiers of Quantitative Verification. In Proc. TOOLympics III, Springer. To appear. 2024. [pdf] [bib] [Write-up of the third edition of QComp, which surveys the state of the art in quantitative verification tools, including PRISM, PRISM-games, and their extensions, amongst many others. ]
[BHK+20] Carlos E. Budde, Arnd Hartmanns, Michaela Klauck, Jan Kretinsky, David Parker, Tim Quatmann, Andrea Turrini and Zhen Zhang. On Correctness, Precision, and Performance in Quantitative Verification: QComp 2020 Competition Report. In Proc. 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'20), volume 12479 of LNCS, pages 216-241, Springer. October 2020. [pdf] [bib] [Summarises the 2020 Comparison of Tools for the Analysis of Quantitative Formal Models (QComp'20) featuring PRISM and 8 other tools.]
[HHH+19] Ernst Moritz Hahn, Arnd Hartmanns, Christian Hensel, Michaela Klauck, Joachim Klein, Jan Křetínský, David Parker, Tim Quatmann, Enno Ruijters and Marcel Steinmetz. The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models (QComp 2019 Competition Report). In Proc. 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19), volume 11429 of LNCS, pages 69-92, Springer. April 2019. [pdf] [bib] [Summarises the first Quantitative Formal Models competition (QComp) featuring PRISM and 8 other tools.]
[HKPQR19] Arnd Hartmanns, Michaela Klauck, David Parker, Tim Quatmann and Enno Ruijters. The Quantitative Verification Benchmark Set. In Proc. 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19), volume 11427 of LNCS, pages 344-350, Springer. April 2019. [pdf] [bib] [Presents a benchmark suite for quantitative verification, include a selection of models/properties for use in PRISM.]
[KNP12b] Marta Kwiatkowska, Gethin Norman and David Parker. The PRISM Benchmark Suite. In Proc. 9th International Conference on Quantitative Evaluation of SysTems (QEST'12), pages 203-204, IEEE CS Press. September 2012. [pdf] [bib] [Introduces a suite of PRISM models/properties and other resources for benchmarking and testing.]
[SUH+06] H. Sauro, A. Uhrmacher, D. Harel, M. Hucka, M. Kwiatkowska, P. Mendes, C. Shaffer, L. Stromback and J. Tyson. Challenges for modeling and simulation methods in systems biology. In L. Perrone, F. Wieland, J. Liu, B. Lawson, D. Nicol and R. Fujimoto (editors), Proc. 2006 Winter Simulation Conference, pages 1720-1730, IEEE. December 2006. [pdf] [bib]
[KNP06e] M. Kwiatkowska, G. Norman and A. Pacheco. Model Checking Expected Time and Expected Reward Formulae with Random Time Bounds. Computers & Mathematics with Applications, 51(2), pages 305-316, Elsevier. January 2006. [ps.gz] [pdf] [bib]
[KNP02d] M. Kwiatkowska, G. Norman and A. Pacheco. Model Checking Expected Time and Expected Reward Formulae with Random Time Bounds. In Proc. 2nd Euro-Japanese Workshop on Stochastic Risk Modelling for Finance, Insurance, Production and Reliability. September 2002. [ps.gz] [pdf] [bib]
[KMNP02] Marta Kwiatkowska, Rashid Mehmood, Gethin Norman and David Parker. A Symbolic Out-of-Core Solution Method for Markov Models. In Proc. Workshop on Parallel and Distributed Model Checking (PDMC'02), volume 68.4 of ENTCS. August 2002. [ps.gz] [pdf] [bib]
[KNP02c] M. Kwiatkowska, G. Norman and A. Pacheco. Model Checking CSL Until Formulae with Random Time Bounds. In H. Hermanns and R. Segala (editors), Proc. PAPM/PROBMIV'02, volume 2399 of Lecture Notes in Computer Science, pages 152-168, Springer. July 2002. [ps.gz] [pdf] [bib]
[KM02] M. Kwiatkowska and R. Mehmood. Out-of-Core Solution of Large Linear Systems of Equations arising from Stochastic Modelling. In Proc. PAPM/PROBMIV'02, volume 2399 of LNCS, pages 135-151, Springer-Verlag. July 2002. [ps.gz] [bib]

Sort by: date, type, title, subject