PRISM-games: Publications

Underlying models, logics and algorithms for 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.]
[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.]
[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.]
[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.]
[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.]
[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+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.]
[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.]

Case studies using PRISM-games

[Ray22] Kaustabha Ray. Policy Design and Verification for Multi-Access Edge Computing: A Formal Methods Perspective. Ph.D. thesis, Indian Statistical Institute, Kolkata. 2022. [Presents verification techniques for multi-access edge computing, building upon PRISM and PRISM-games.]
[RB22a] Kaustabha Ray and Ansuman Banerjee. Prioritized Fault Recovery Strategies for Multi-Access Edge Computing Using Probabilistic Model Checking. IEEE Transactions on Dependable and Secure Computing. 2022. [Uses PRISM-games combined with heuristics to generate fault-recovery strategies for Multi-Access Edge Computing.]
[RB21] Kaustabha Ray and Ansuman Banerjee. Modeling and Verification of Service Allocation Policies for Multi-Access Edge Computing Using Probabilistic Model Checking. IEEE Transactions on Network and Service Management. 2021. [Uses PRISM-games to model and verify service allocation policies for multi-access edge computing.]
[RB21b] Kaustabha Ray and Ansuman Banerjee. A Framework for Analyzing Resource Allocation Policies for Multi-Access Edge Computing. In Proc. IEEE International Conference on Edge Computing (EDGE'21), pages 102-110, IEEE. 2021. [Uses PRISM-games to verify resource allocation policies for multi-access edge computing. ]
[DHB21] Jacob Dineen, A. S. M. Ahsan-Ul Haque and Matthew Bielskas. Formal Methods for an Iterated Volunteer’s Dilemma. In Proc. International Conference on Social Computing, Behavioral-Cultural Modeling and Prediction and Behavior Representation in Modeling and Simulation (SBP-BRiMS'21). 2021. [Performs a formal analysis of the iterated volunteer’s dilemma using PRISM-games.]
[GGS20] T. J. Glazier, D. Garlan and B. Schmerl. Automated Management of Collections of Autonomic Systems. In Proc. IEEE International Conference on Autonomic Computing and Self-Organizing Systems (ACSOS'20), pages 82-91. 2020. [Proposes an automated approach to managing multiple autonomic systems, building upon PRISM-games. ]
[WDSX19] Xiaomin Wei, Yunwei Dong, Pengpeng Sun and Mingrui Xiao. Safety Analysis of AADL Models for Grid Cyber-Physical Systems via Model Checking of Stochastic Games. Electronics, 8(2). 2019. [Formally analyses grid cyber-physical systems using PRISM-games.]
[JJK+18] Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu, Ruohan Zhang and Mary Hayhoe. Model Checking for Safe Navigation Among Humans. In Proc. 15th International Conference on Quantitative Evaluation of SysTems (QEST'18), volume 11024 of LNCS, pages 207-222, Springer. 2018. [bib] [Applies probabilistic model checking to autonomous system operating alongside uncontrollable agents such as humans, including use of PRISM-games for stochastic game models.]
[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.]
[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.]
[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.]
[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.]
[CMG15] Javier Cámara, Gabriel A. Moreno and David Garlan. Reasoning about Human Participation in Self-Adaptive Systems. In Proc. 10th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'15). 2015. [Proposes a formal framework for reasoning about human involvement in self-adaptive systems, using PRISM-games as an underlying model checker.]
[GCSG15] Thomas Glazier, Javier Cámara, Bradley Schmerl and David Garlan. Analyzing Resilience Properties of Different Topologies of Collective Adaptive Systems. In Proc. 2015 IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops (SASOW'15), pages 55-60. 2015. [Uses PRISM-games to analyse the impact of communication topologies for collective adaptive systems defending against an external attack.]
[CGSP15] Javier Cámara, David Garlan, Bradley Schmerl and Ashutosh Pandey. Optimal Planning for Architecture-Based Self-Adaptation Via Model Checking of Stochastic Games. In Proc. 30th ACM Symposium on Applied Computing (SAC'15), Dependable and Adaptive Distributed Systems (DADS) track. 2015. [bib] [Proposes techniques for architecture-based self-adapation using stochastic multi-player games and PRISM-games.]
[DKSS14] Tushar Deshpande, Panagiotis Katsaros, Scott Smolka and Scott Stoller. Stochastic Game-Based Analysis of the DNS Bandwidth Amplification Attack Using Probabilistic Model Checking. In Proc. 10th European Dependable Computing Conference (EDCC'14). 2014. [Analyses the DNS bandwidth amplification attack using a stochastic game model and PRISM-games.]
[CMG14] Javier Cámara, Gabriel A. Moreno and David Garlan. Stochastic Game Analysis and Latency Awareness for Proactive Self-Adaptation. In Proc. 9th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'14), pages 155-164, ACM. 2014. [Uses PRISM-games to analyse adaptation tactic latency in self-adaptive systems.]
[CGMS13] Javier Camara, David Garlan, Gabriel Moreno and Bradley Schmerl. Analyzing Self-adaptation Via Model Checking of Stochastic Games. In Software Engineering for Self-Adaptive Systems, Springer. 2013. [Describes an approach for the analysis of self-adaptive systems using PRISM-games.]
[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.]
[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.]
[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.]

Techniques and tools building on PRISM-games

[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.]
[ST21] Georg Friedrich Schuppe and Jana Tumova. Decentralized Multi-Agent Strategy Synthesis under LTLf Specifications via Exchange of Least-Limiting Advisers. In Proc. 2021 International Symposium on Multi-Robot and Multi-Agent Systems (MRS), pages 119-127. 2021. [Proposes techniques for multi-agent task-planning implemented in a tool chain incorporating PRISM-games.]
[KM20] William Kavanagh and Alice Miller. Gameplay Analysis of Multiplayer Games with Verified Action‐Costs. The Computer Games Journal, 10, pages 89-110. 2021. [bib] [Proposes techniques for measuring the skill levels of players in a game, including the use of PRISM-games.]
[CKWW20] Krishnendu Chatterjee, Joost-Pieter Katoen, Maximilian Weininger and Tobias Winkler. Stochastic Games with Lexicographic Reachability-Safety Objectives. In Proc. 32nd International Conference on Computer Aided Verification (CAV'20), volume 12225 of LNCS, pages 398-420, Springer. 2020. [bib] [Develops a solving lexicographic reachability-safety objectives on stochastic games, implemented as an extension of PRISM-games.]
[LP20] Alessio Lomuscio and Edoardo Pirovano. Parameterised Verification of Strategic Properties in Probabilistic Multi-Agent Systems. In Proc. 19th International Conference on Autonomous Agents and Multiagent Systems (AAMAS'20), pages 762-770. 2020. [Develops techniques and a tool for verifying parameterised probabilistic multi-agent systems, building upon PRISM and PRISM-games.]
[LCGS20] Nianyu Li, Javier Cámara, David Garlan and Bradley Schmerl. Reasoning about When to Provide Explanation for Human-involved Self-Adaptive Systems. In Proc. IEEE International Conference on Autonomic Computing and Self-Organizing Systems (ACSOS'20). 2020. [Reasons about self-adaptive systems with human involvement using probabilistic model checking and PRISM-games.]
[IIZ20] Azlan Ismail, Susanti Intu and Suzana Zambri. A GUI-driven prototype for synthesizing self-adaptation decision. Bulletin of Electrical Engineering and Informatics. 2020. [Proposes a decision-making approach for self-adapative systems implemented on top of PRISM-games.]
[PTHH20] Kittiphon Phalakarn, Toru Takisaka, Thomas Haas and Ichiro Hasuo. Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games. In Proc. 32nd International Conference on Computer Aided Verification (CAV'20), volume 12225 of LNCS, pages 349-371, Springer. 2020. [bib] [Develops a bounded value iteration technique for accurate solution of stochastic games, implemented as an extension of PRISM-games.]
[ZH19] Hein Htoo Zaw and Swe Zin Hlaing. Verifying the Gaming Strategy of Self-learning Game by Using PRISM-Games. In Proc. International Conference on Intelligent Computing & Optimization (ICO'19), volume 1072 of AISC, pages 148-159. 2019. [Studies learning based approaches for MDP policy synthesis, using PRISM-games as a model checker.]
[EK19] Julia Eisentraut and Jan Kretinsky. Expected Cost Analysis of Attack-Defense Trees. In Proc. 16th International Conference on Quantitative Evaluation of Systems (QEST'19), volume 11785 of LNCS, pages 203-221, Springer. 2019. [bib] [Presents an approach to analysing attack-defence trees using PRISM-games for model checking stochastic games.]
[CPGS18] Javier Cámara, Wenxin Peng, David Garlan and Bradley Schmerl. Reasoning about sensing uncertainty and its reduction in decision-making for self-adaptation. Science of Computer Programming, 167, pages 51-69, Elsevier. 2018. [Proposes a formal analysis technique for self-adaptive decision making under sensor uncertainty, building on the PRISM-games framework.]
[WJW+17] Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen and Bernd Becker. Motion Planning under Partial Observability using Game-Based Abstraction. In Proc. 56th Annual Conference on Decision and Control (CDC'17), pages 2201-2208, IEEE. 2017. [Develops a game-based abstraction approach to solving POMDPs, including PRISM-games as part of the tool-chain.]
[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.]

Tool papers

[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.]

Survey/tutorial papers

[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.]
[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.]
[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.]

PRISM-games: Publications

Contents:

Underlying models, logics and algorithms for PRISM-games

Case studies using PRISM-games

Techniques and tools building on PRISM-games

Tool papers

Survey/tutorial papers

PRISM-games