Underlying models, logics and algorithms for PRISM-games
[KNPS20c]Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos.Automatic Verification of Concurrent Stochastic Systems.Formal Methods in System Design, Springer. To appear.January 2021.
[pdf]
[bib]
[Proposes verification techniques for concurrent stochastic games, and implements and evaluates them in an extension of 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. To appear.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.]
[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+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+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
[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.
]
[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.]
[CGSP15]Javier Cá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.[Proposes techniques for architecture-based self-adapation using stochastic multi-player games and PRISM-games.]
[GCSG15]Thomas Glazier, Javier Cá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.]
[CMG15]Javier Cá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.]
[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.]
[CMG14]Javier Cá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.]
[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
[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.]
[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.[Develops a solving lexicographic reachability-safety objectives on stochastic games, implemented as an extension 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.]
[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.]
[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.]
[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.]
[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.]
Site hosted at the Department of Computer Science, University of Oxford