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.

414 publications:

2014

  • [CS14] Muffy Calder and Michele Sevegnani. Modelling IEEE 802.11 CSMA/CA RTS/CTS with stochastic bigraphs with sharing. Formal Aspects of Computing, 26(3), pages 537-561. 2014. [Analyses a model of the 802.11 CSMA/CA RTS/CTS protocol, modelled in an extension of stochastic bigraphical reactive systems, and then imported into PRISM]
  • [FYO14] Ling Fang, Yoriyuki Yamagata and Yutaka Oiwa. Evaluation of A Resilience Embedded System Using Probabilistic Model-Checking. In Proc. 3rd International Workshop on Engineering Safety and Security Systems 2014 (ESSS'14), volume 150 of EPTCS, pages 35-49. 2014. [Uses probabilistic model checking and PRISM to analyse resilience strategies for micro processor units.]
  • [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.]
  • [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). To appear. November 2014. [bib] [Presents MDP verification techniques, implemented in PRISM, based on real-time dynamic programming and delayed Q-learning.]
  • [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), 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.]
  • [DKPQ14] Klaus Draeger, Marta Kwiatkowska, David Parker and Hongyang Qu. Local Abstraction Refinement for Probabilistic Timed Programs. Theoretical Computer Science, 538, pages 37–53. 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.]
  • [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.]
  • [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.]
  • [OMD14] Samir Ouchania, Otmane Aït Mohameda and Mourad Debbabi. A property-based abstraction framework for SysML activity diagrams. Knowledge-Based Systems, 6, pages 328-343. January 2014. [Presents methods to abstract and verify SysML activity diagrams using PRISM as a back-end.]
  • [KT14] Marta Kwiatkowska and Chris Thachuk. Probabilistic Model Checking for Biology. In Software Safety and Security, IOS Press. To appear. 2014. [pdf] [bib] [A tutorial on the application of probabilistic model checking and PRISM to biological systems.]
  • [DKTT14] Frits Dannenberg, Marta Kwiatkowska, Chris Thachuk and Andrew J. Turberfield. DNA walker circuits: Computational potential, design, and verification. Natural Computing. To appear. 2014. [pdf] [bib] [Designs a discrete stochastic model of DNA walker circuits and analyses it with probabilistic model checking and PRISM.]

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

2000

Publications