www.prismmodelchecker.org

PRISM Bibliography

The following is a bibliography of PRISM-related papers. This includes both papers from the PRISM team and from elsewhere.

See also the separate lists of PRISM-related papers produced externally and by the PRISM team, and the list of selected PRISM papers.

If there is something we have omitted, please contact us.

539 publications:

Case studies using PRISM

2018
2017
2016
2015
2014
2013
2012
2011
2010
2009
2008
2007
2006
2005
2004
2003
2002
2001

Underlying techniques in PRISM

2017
2016
  • [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.]
2015
  • [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.]
  • [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.]
  • [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.]
2014
  • [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.]
2013
  • [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+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.]
  • [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.]
2012
  • [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.]
2010
2009
  • [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.]
2008
2007
2006
2005
2004
2003
2002
2001
2000

Extensions and adaptions to PRISM

2018
2017
2016
  • [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.]
  • [KBC+16] Joachim Klein, Christel Baier, Philipp Chrszon, Marcus Daum, Clemens Dubslaff, Sascha Klüppelholz and Steffen Märcker, David Müller. Advances in Symbolic Probabilistic Model Checking with PRISM. In Proc. 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16), pages 349-366, Springer. 2016. [Presents a collection of extensions to PRISM, including automatic variable reordering, reward-based properties and automata improvements. ]
  • [KKR16] Lubos Korenciak, Antonin Kucera and Vojtech Rehak. Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration. In Proc. 24th IEEE International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS'16). 2016. [Proposes fixed-delay synthesis techniques on a variant of continuous-time Markov chains, implemented as 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), Springer. To appear. April 2016. [pdf] [bib] [Introduces an extension of PRISM in the form of GPU-accelerated tool for parameter synthesis of stochastic systems. ]
2015
  • [BCFK15] Tomáš Brázdil, Krishnendu Chatterjee, Vojtěch Forejt and Antonín Kučera. MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives. In Proc. 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15), volume 9035 of LNCS, pages 181-187, Springer. 2015. [Presents a tool for multi-objective model checking of mean-payoff properties MDPs, building on several PRISM components.]
  • [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.]
2014
2013
  • [Tsa13] Tony Tsang. Performance Analysis for QoS-Aware Two- Layer Scheduling in LTE Networks. International Journal of Emerging Trends & Technology in Computer Science (IJETTCS), 2(2). 2013. [Uses an extension of PRISM's simulator to solve scheduling and resource allocation problems.]
  • [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.]
2012
  • [BDE+12] Christel Baier, Marcus Daum, Benjamin Engel, Hermann Härtig, Joachim Klein, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews and Marcus Völp. Waiting for Locks: How Long Does It Usually Take?. In Proc. 17th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'12). 2012. [Extends PRISM with support for conditional steady-state queries and then analyses models of low-level operating-system code, using a test-and-test-and-set (TTS) lock as an example.]
  • [WB12] Anton Wijs and Dragan Bosnacki. Improving GPU Sparse Matrix-Vector Multiplication for Probabilistic Model Checking. In A. Donaldson and D. Parker (editors), Proc. 19th International SPIN Workshop on Model Checking of Software (SPIN'12), volume 7385 of LNCS, pages 98-116, Springer. 2012.
  • [HMZ+12] David Henriques, Joao G. Martins, Paolo Zuliani, André Platzer and Edmund M. Clarke. Statistical Model Checking for Markov Decision Processes. In Proc. 9th International Conference on Quantitative Evaluation of SysTems (QEST'12). 2012. [Develops techniques for statistical model checking of MDPs, built with an extension to PRISM's simulation engine.]
  • [vEJ12] Christian von Essen and Barbara Jobstmann. Synthesizing Efficient Controllers. In Proc. 13th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'12), volume 7148 of LNCS, pages 428-444, Springer. 2012. [bib] [Presents MDP-based controller synthesis techniques for ratio objectives and implements them in 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.]
2011
2010
2009
2008
  • [ZHHW08] L. Zhang, H. Hermanns, E. M. Hahn and B. Wachter. Time-bounded model checking of infinite-state continuous-time Markov chains. In Proc. 8th International Conference on Application of Concurrency to System Design (ACSD'08), pages 98-107. 2008. [bib]
  • [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.]
2007
2005
2004

Tool/language connections to PRISM

2018
2017
2016
  • [CDKB16] Philipp Chrszon, Clemens Dubslaff, Sascha Klüppelholz and Christel Baier. Family-Based Modeling and Analysis for Probabilistic Systems - Featuring ProFeat. In Proc. 19th International Conference on Fundamental Approaches to Software Engineering (FASE'16), volume 9633 of LNCS, pages 287-304, Springer. 2016. [Proposes a formalism for modelling families of probabilistic systems with differing features and a tool for their analysis, which connects to PRISM through model translations.]
  • [MRAAB16] Danilo Filgueira Mendonça, Genaína Nunes Rodriguesa, Raian Alib, Vander Alvesa and Luciano Baresi. GODA: A goal-oriented requirements engineering framework for runtime dependability analysis. Information and Software Technology, 80, pages 245–264, Elsevier. 2016. [Proposes GODA, a goal-oriented requirements engineering framework for runtime dependability analysis, which uses probabilistic model checking and PRISM for underlying analysis. ]
  • [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.]
2015
  • [PLK+15] Jaime Pulido Fentanes, Bruno Lacerda, Tomas Krajnik, Nick Hawes and Marc Hanheide. Now or later? Predicting and Maximising Success of Navigation Actions from Long-Term Experience. In Proc. 2015 IEEE International Conference on Robotics and Automation (ICRA'14). 2015. [Proposes novel approaches to predicting changes in a robot's environment, applied to a probabilistic planning framework using PRISM as an underlying solver.]
  • [NSG+15] Athanasios Naskos, Emmanouela Stachtiari, Anastasios Gounaris, Panagiotis Katsaros, Dimitrios Tsoumakos, Ioannis Konstantinou and Spyros Sioutas. Dependable Horizontal Scaling Based On Probabilistic Model Checking. In Proc. 15th IEEE/ACM International Symposium on Cluster, Cloud and Grid Computing (CCGrid'15). 2015. [Uses probabilistic model checking and PRISM for cloud elasticity, i.e. on-demand resource provisioning in cloud computing.]
  • [CGB15] Radu Calinescu, Simos Gerasimou and Alec Banks. Self-Adaptive Software with Decentralised Control Loops. In Proc. 18th International Conference on Fundamental Approaches to Software Engineering (FASE'15). 2015. [Presents an approach for decentralised control of self-adaptive systems, using PRISM as an underlying model checker.]
  • [CGLG15] Zack Coker, David Garlan and Claire Le Goues. SASS: Self-adaptation using stochastic search. In Proc. 10th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'15). 2015. [Proposes the use of stochastic search techniques for self-adaptive systems, illustrated with a genetic algorithm that uses PRISM to compute fitness functions.]
  • [NS15] Bojan Nokovic and Emil Sekerinski. A Holistic Approach in Embedded System Development. In Proc. 2nd International Workshop on Formal Integrated Development Environment (F-IDE'15). 2015. [Presents pState, a tool for development of embedded systems, which uses PRISM for model analysis and verification.]
  • [GTC15] Simos Gerasimou, Giordano Tamburrelli and Radu Calinescu. Search-Based Synthesis of Probabilistic Models for Quality-of-Service Software Engineering. In Proc. 30th IEEE/ACM International Conference on Automated Software Engineering (ASE'15). 2015. [Proposes search-based software engineering techniques using multi-objective optimisation, implemented in the EvoChecker tool which performs model analysis using PRISM.]
  • [LMO15] Gabriele Lenzini, Sjouke Mauw and Samir Ouchani. Security Analysis of Socio-Technical Physical Systems. Computers & Electrical Engineering, Elsevier. 2015. [Proposes an approach to detect and quantify attacks in socio-technical physical systems, using a mapping to PRISM.]
  • [CGJ+15] Radu Calinescu, Carlo Ghezzi, Kenneth Johnson, Mauro Pezzé, Yasmin Rafiq and Giordano Tamburrelli. Formal Verification With Confidence Intervals to Establish Quality of Service Properties of Software Systems. IEEE Transactions on Reliability. 2015. [Uses PRISM as part of a tool chain formally verify QoS properties of software systems.]
  • [KG15] Savas Konur and Marian Gheorghe. A Property-Driven Methodology for Formal Analysis of Synthetic Biology Systems. IEEE/ACM Transactions on Computational Biology and Informatics. 2015. [Proposes a framework for formal analysis of synthetic biology systems, which includes use of PRISM for probabilistic model checking.]
2014
2013
  • [CDF+13] Andrea Ciancone, Mauro Luigi Drago, Antonio Filieri, Vincenzo Grassi, Heiko Koziolek and Raffaela Mirandola. The KlaperSuite Framework for Model-Driven Reliability Analysis of Component-Based Systems. Software & Systems Modeling. 2013. [Describes the KlaperSuite framework for model-driven reliability analysis, which builds on several tools including PRISM.]
  • [KJR13] Radu Calinescu, Kenneth Johnson and Yasmin Rafiq. Developing Self-Verifying Service-Based Systems. In Proc. 28th IEEE/ACM International Conference on Automated Software Engineering (ASE'13), IEEE. 2013. [Describes a self-verifying framework for service-based systems, including PRISM as a backend solver.]
  • [SGO13] Simon Struck, Matthias Gudemann and Frank Ortmeier. Efficient Optimization of Large Probabilistic Models. Journal of Systems and Software. 2013. [Presents a framework for modelling, analysis and optimization of safety critical systems, which connects to PRISM.]
  • [ZREF13] Fokion Zervoudakis, David S. Rosenblum, Sebastian Elbaum and Anthony Finkelstein. Cascading Verification: An Integrated Method for Domain-Specific Model Checking. In Proc. 9th Joint Meeting on Foundations of Software Engineering (ESEC/FSE'13), pages 400-410 , ACM. 2013. [Proposes a domain-specific model checking framework, including PRISM as an underlying solver.]
  • [FBZ13] João Franco, Raul Barbosa and Mário Zenha Rela. Reliability analysis of software architecture evolution. In Proc. Latin-American Symposium on Dependable Computing (LADC'13). 2013. [Analyses quality attributes of software architectures by translating an architecture design language into PRISM. ]
  • [JCK13] Kenneth Johnson, Radu Calinescu and Shinji Kikuchi. An Incremental Verification Framework for Component-Based Software Systems. In Proc. 16th International ACM Sigsoft symposium on Component-based software engineering (CBSE'13), pages 33-42. 2013. [Presents a framework for the efficient reverification of component-based software system, with a software prototype built on top of PRISM.]
  • [RBC+13] Neha Rungta, Guillaume Brat, William J. Clancey, Charlotte Linde, Franco Raimondi, Chin Seah and Michael Shafto. Aviation Safety: Modeling and Analyzing Complex Interactions between Humans and Automated Systems. In Proc. International Conference on Application and Theory of Automation in Command and Control Systems (ATACCS'13). 2013. [Presents a verification approach based on the Brahms multi-agent framework, with connections to several model checkers, including PRISM.]
  • [HRRS13] Josie Hunter, Franco Raimondi, Neha Rungta and Richard Stocker. A synergistic and extensible framework for multi-agent system verification. In Proc. International conference on Autonomous Agents and Multi-Agent Systems (AAMAS'13). 2013. [Presents a verification approach based on the Brahms multi-agent framework, with connections to several model checkers, including PRISM.]
  • [PLSVS13] Alberto Puggelli, Wenchao Li, Alberto L. Sangiovanni-Vincentelli and Sanjit A. Seshia. Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties. In Proc. 25th International Conference on Computer Aided Verification (CAV'13). 2013. [Develops techniques for verification of MDPs with convex uncertainties, implemented through an interface to PRISM.]
  • [HS13] Luke Herbert and Robin Sharp. Precise Quantitative Analysis of Probabilistic Business Process Model and Notation Workflows. J. Comput. Inf. Sci. Eng., 13(1). 2013. [Translates a subset of the Business Process Modelling and Notation (BPMN) language into PRISM, to allow probabilistic model checking of business workflows.]
  • [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.]
2012
2011
2010
2009
2008
2007
2006
2005
2004
2003
2002

PRISM tool papers

2018
2016
2013
  • [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.]
2011
2006
  • [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.]
2004
2002
  • [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.]
2001
  • [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

2017
  • [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.]
2016
2014
  • [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.]
2013
  • [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. ]
2012
  • [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.]
2011
  • [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.]
2010
  • [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.]
2009
  • [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.]
2008
2007
  • [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.]
2004
2003

Others

2016
2014
  • [HBHS14] Fenglin Han, Jan Olaf Blech, Peter Herrmann and Heinz Schmidt. Towards Verifying Safety Properties of Real-Time Probabilistic Systems. In Proc. Formal Engineering Approaches to Software Components and Architectures (FESCA'14), EPTCS. 2014. [Presents an extension of the Reactive Blocks tool set for analysing probabilistic real-time systems, through a connection to 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.]
  • [JD14] Yosr Jarraya and Mourad Debbabi. Quantitative and qualitative analysis of SysML activity diagrams. International Journal on Software Tools for Technology Transfer, 16(4), pages 399-419. 2014. [Presents a framework for probabilistic verification of SysML activity diagrams via a translation to PRISM.]
  • [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.]
  • [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.]
  • [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.]
2012
  • [BDE+12b] Christel Baier, Marcus Daum, Benjamin Engel, Hermann Härtig, Joachim Klein, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews and Marcus Völp. Chiefly Symmetric: Results on the Scalability of Probabilistic Model Checking for Operating-System Code. In Proc. 7th Conference on Systems Software Verification (SSV'12), volume 102 of EPTCS. 2012. [Investigates symmetry reduction techniques for probabilistic model checking using models build with 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.]
2011
2006
2004
2003
2002
2000

Publications