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.

768 publications:









  • [MHGSH16] Awais Mahmood, Osman Hasan, Hassan Raza Gillani, Yassar Saleem and Syed Rafay Hasan. Formal reliability analysis of protective systems in smart grids. In Proc. 2016 IEEE Region 10 Symposium (TENSYMP). 2016. [Provides a reliability assessment of smart grids using PRISM.]
  • [AC16] Jose Ignacio Aizpurua and Victoria M. Catterson. ADEPS: A Methodology for Designing Prognostic Applications. In Proc. 3rd European Conference of the Prognostics and Health Management Society. 2016. [Proposes ADEPS (Assisted Design for Engineering Prognostic Systems), which uses PRISM as an underlying verification tool.]
  • [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.]
  • [TMSR16] Pedro J. Rivera Torres, Eileen I. Serrano Mercado, Orestes Llanes Santiago and Luis Anido Rifon. Modeling preventive maintenance of manufacturing processes with probabilistic Boolean networks with interventions. Journal of Intelligent Manufacturing, Springer. 2016. [Proposes techniques based on probabilistic Boolean networks to analyse manufacturing processes, and uses PRISM as an underlying tool.]
  • [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. [bib] [Presents a collection of extensions to PRISM, including automatic variable reordering, reward-based properties and automata improvements. ]
  • [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.]
  • [SK16] Maria Svorenova and Marta Kwiatkowska. Quantitative Verification and Strategy Synthesis for Stochastic Games. European Journal of Control, Elsevier. To appear. 2016. [pdf] [bib] [Provides an overview of techniques for quantitative verification and strategy synthesis for stochastic games.]
  • [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.]
  • [PMCG16] Ashutosh Pandey, Gabriel A. Moreno, Javier Cámara and David Garlan. Hybrid Planning for Decision Making in Self-Adaptive Systems. In Proc. 10th International Conference on Self-Adaptive and Self-Organizing Systems (SASO'16). 2016. [Presents a hybrid planning technique for self-adaptive systems combining learning and probabilistic model checking, with an implementation based on PRISM.]
  • [GBKF16] Safa Guellouz, Adel Benzina, Mohamed Khalgui, Georg Frey. ZiZo: A Complete Tool Chain for the Modeling and Verification of Reconfigurable Function Blocks. In Proc. 10th International Conference on Mobile Ubiquitous Computing, Systems, Services and Technologies (UBICOMM'16). 2016. [Presents a tool-chain for modelling and verification of reconfigurable distributed system, using PRISM as a back-end verifier.]
  • [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.]
  • [KRF16] Lubos Korenciak, Vojtech Rehak and Adrian Farmadin. Extension of PRISM by Synthesis of Optimal Timeouts in Fixed-Delay CTMC. In Proc. 12th International Conference on Integrated Formal Methods (IFM'16), volume 9681 of LNCS, pages 130-138, Springer. 2016. [Presents an extension of PRISM to support fixed-delay continuous-time Markov chains (fdCTMCs).]
  • [SSB+16] Dongwon Seo, Donghwan Shin, Young-Min Baek, Jiyoung Song, Wonkyung Yun, Junho Kim, Eunkyoung Jee and Doo-Hwan Bae. Modeling and Verification for Different Types of System of Systems using PRISM. In Proc. IEEE/ACM 4th International Workshop on Software Engineering for Systems-of-Systems (SESoS'16), pages 12-18. 2016. [Proposes a modelling scheme for system of systems (SoS) and uses PRISM for verification.]
  • [IQV16] Paolo Izzo, Hongyang Qu and Sandor M. Veres. A stochastically verifiable autonomous control architecture with reasoning. In Proc. IEEE Conference on Decision and Control (CDC'16). 2016. [Proposes an architecture for autonomous control with underlying verification abilities provided by PRISM.]
  • [NGMK16] Athanasios Naskos, Anastasios Gounaris, Haralambos Mouratidis and Panagiotis Katsaros. Online analysis of security risks in elastic cloud applications using probabilistic model checking. IEEE Cloud Computing Magazine. 2016. [Analyses the trade-offs between security risks and performance in cloud computing systems using probabilistic model checking and PRISM.]
  • [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.]
  • [SAH+16] Muhammad Usama Sardar, Nida Afaq, Khaza Anuarul Hoque, Taylor T. Johnson and Osman Hasan. Probabilistic Formal Verification of the SATS Concept of Operation. In Proc. 8th International Symposium on NASA Formal Methods (NFM'16), volume 9690 of LNCS, pages 191–205, Springer. 2016. [Presents a formal analysis of NASA's Small Aircraft Transportation System (SATS) technology using probabilistic model checking and PRISM.]
  • [PLM16] Zhaoguang Peng, Yu Lu and Alice Miller. Uncertainty Analysis of Phased Mission Systems with Probabilistic Timed Automata. In Proc. 7th IEEE International Conference on Prognostics and Health Management (PHM'16). 2016. [Analyses phased mission requirements using probabilistic timed automata and PRISM.]
  • [GDH16] Paul Gainer, Clare Dixon and Ullrich Hustadt. Probabilistic Model Checking of Ant-Based Positionless Swarming. In Proc. Towards Autonomous Robotic Systems (TAROS'16). 2016. [Uses probabilistic model checking and PRISM to study control algorithms for robot swarms.]
  • [BKdM+16] Christel Baier, Sascha Klüppelholz, Hermann de Meer, Florian Niedermeier and Sascha Wunderlich. Greener Bits: Formal Analysis of Demand Response. In Proc. 14th International Symposium on Automated Technology for Verification and Analysis (ATVA'16), pages 323-339, Springer. 2016. [Develops formal techniques for managing demand response in power generation, including a probabilistic analysis 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.]
  • [GEK16] Sotirios Gyftopoulos, Pavlos S. Efraimidis and Panagiotis Katsaros. Solving Influence Problems on the DeGroot Model with a Probabilistic Model Checking Tool. In Proc. 20th Pan-Hellenic Conference on Informatics (PCI'16). 2016. [Uses PRISM-games to analyse the DeGroot model of opinion diffusion and formation in social networks.]
  • [AH16] Mohammed Alabdullatif and Reiko Heckel. Graph Transformation Games for Negotiating Features. In Proc. Graphs as Models 2016. 2016. [Proposes a negotiation game for designing flexible business interactions, with an underlying analysis based on PRISM-games.]
  • [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. ]
  • [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. [bib] [Gives an overview of quantitative verification and strategy synthesis for stochastic multi-player games, as implemented in PRISM-games.]
  • [LZW+16] Lulu Liang, Kai Zheng, Zilong Wei, Yanmei Wang, Sihan Wu and Xin Huang. Model Checking of IoT System in Microgrid. In Proc. IEEE International Symposium on Information in Medicine and Education (ITME'16). 2016. [Verifies the reliability of IoT systems in microgrids using probabilistic model checking and PRISM.]
  • [CJP16] Radu Calinescu, Kenneth Johnson and Colin Paterson. FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals. In Proc. TACAS'16, volume 9636 of LNCS, pages 540-546, Springer. 2016. [Presents a model checker for computing confidence intervals, building on PRISM's parametric model checking functionality.]
  • [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.]
  • [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.]
  • [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.]
  • [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.]
  • [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. ]
  • [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.]