Document Open Access Logo

Model Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice (Invited Talk)

Author Marta Z. Kwiatkowska

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2016.4.pdf
  • Filesize: 0.6 MB
  • 18 pages

Document Identifiers

Author Details

Marta Z. Kwiatkowska

Cite As Get BibTex

Marta Z. Kwiatkowska. Model Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice (Invited Talk). In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.ICALP.2016.4

Abstract

Probabilistic model checking is an automatic procedure for establishing if a desired property holds in a probabilistic model, aimed at verifying quantitative probabilistic specifications such as the probability of a critical failure occurring or expected time to termination. 

Much progress has been made in recent years in algorithms, tools and applications of probabilistic model checking, as exemplified by the probabilistic model checker PRISM (http://www.prismmodelchecker.org). However, the unstoppable rise of autonomous systems, from robotic assistants to self-driving cars, is placing greater and greater demands on quantitative modelling and verification technologies. To address the challenges of autonomy we need to consider collaborative, competitive and adversarial behaviour, which is naturally modelled using game-theoretic abstractions, enhanced with stochasticity arising from randomisation and uncertainty. This paper gives an overview of quantitative verification and strategy synthesis techniques developed for turn-based stochastic multi-player games, summarising recent advances concerning multi-objective properties and compositional strategy synthesis. The techniques have been implemented in the PRISM-games model checker built as an extension of PRISM.

Subject Classification

Keywords
  • Quantitative verification
  • Stochastic games
  • Temporal logic
  • Model checking
  • Strategy synthesis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. R. Alur, T. Henzinger, and O. Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):672-713, 2002. Google Scholar
  2. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. Google Scholar
  3. Tobias Amnell, Gerd Behrmann, Johan Bengtsson, Pedro R. D'Argenio, Alexandre David, Ansgar Fehnker, Thomas Hune, Bertrand Jeannet, Kim G. Larsen, M. Oliver Möller, Paul Pettersson, Carsten Weise, and Wang Yi. Uppaal - Now, Next, and Future. In F. Cassez, C. Jard, B. Rozoy, and M. Ryan, editors, Modelling and Verification of Parallel Processes, number 2067 in Lecture Notes in Computer Science Tutorial, pages 100-125. Springer-Verlag, 2001. Google Scholar
  4. Daniel Andersson and Peter Bro Miltersen. The Complexity of Solving Stochastic Games on Graphs. In Algorithms and Computation, volume 5878 of LNCS, pages 112-121. 2009. Google Scholar
  5. Zaruhi Aslanyan, Flemming Nielson, and David Parker. Quantitative Verification and Synthesis of Attack-Defence Scenarios. In Proc. of Computer Security Foundations Symposium CSF, 2016. to appear. Google Scholar
  6. Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella. The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming, 72(1–2):3-21, 2008. Google Scholar
  7. C. Baier, E. Clarke, V. Hartonas-Garmhausen, M. Kwiatkowska, and M. Ryan. Symbolic model checking for probabilistic processes. In P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, editors, Proc. 24th Int. Colloq. Automata, Languages and Programming (ICALP'97), volume 1256 of LNCS, pages 430-440. Springer, 1997. Google Scholar
  8. S. Basagiannis, P. Katsaros, A. Pombortsis, and N. Alexiou. Probabilistic model checking for the quantification of DoS security threats. Computers &Security, 2009. Google Scholar
  9. N. Basset, M. Kwiatkowska, and C. Wiltsche. Compositional strategy synthesis for stochastic games with multiple objectives. Technical Report CS-RR-16-03, Department of Computer Science, University of Oxford, 2016. Google Scholar
  10. Nicolas Basset, Marta Z. Kwiatkowska, Ufuk Topcu, and Clemens Wiltsche. Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives. In Proc. of Tools and Algorithms for the Construction and Analysis of Systems TACAS, pages 256-271, 2015. Google Scholar
  11. Nicolas Basset, Marta Z. Kwiatkowska, and Clemens Wiltsche. Compositional Controller Synthesis for Stochastic Games. In Proc. of Concurrency Theory CONCUR, pages 173-187, 2014. Google Scholar
  12. Andrea Bianco and Luca de Alfaro. Model checking of probabilistic and nondeterministic systems. In Proc. of Foundations of Software Technology and Theoretical Computer Science FSTTCS, volume 1026 of LNCS, pages 499-513, 1995. Google Scholar
  13. P. Billingsley. Probability and Measure. Wiley, 1995. Google Scholar
  14. Tomás Brázdil, Václav Brozek, Vojtech Forejt, and Antonín Kucera. Stochastic Games with Branching-Time Winning Objectives. In Proc. of Logic in Computer Science LICS, pages 349-358, 2006. Google Scholar
  15. R. Calinescu, C. Ghezzi, M. Kwiatkowska, and R. Mirandola. Self-adaptive software needs quantitative verification at runtime. Communications of the ACM, 55(9):69-77, 2012. Google Scholar
  16. Javier Cámara, Gabriel A. Moreno, and David Garlan. Stochastic Game Analysis and Latency Awareness for Proactive Self-adaptation. In Proc. of Software Engineering for Adaptive and Self-Managing Systems SEAMS, pages 155-164, 2014. Google Scholar
  17. M. Ceska, F. Dannenberg, N. Paoletti, M. Kwiatkowska, and L. Brim. Precise parameter synthesis for stochastic biochemical systems. Acta Informatica, to appear, 2016. Google Scholar
  18. Krishnendu Chatterjee and Laurent Doyen. Partial-Observation Stochastic Games: How to Win when Belief Fails. Transactions on Compuational Logic, 15(2):16, 2014. Google Scholar
  19. Krishnendu Chatterjee and Laurent Doyen. Perfect-information Stochastic Games with Generalized Mean-Payoff Objectives. In Proc. of LICS. 2016. To appear. Google Scholar
  20. Krishnendu Chatterjee, Laurent Doyen, Sumit Nain, and Moshe Y. Vardi. The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies. In Proc. of Foundations of Software Science and Computation Structures FOSSACS, pages 242-257, 2014. Google Scholar
  21. Krishnendu Chatterjee and Thomas A. Henzinger. A survey of stochastic ω-regular games. Journal of Computer and System Sciences, 78(2):394-413, 2012. Google Scholar
  22. Krishnendu Chatterjee and Rasmus Ibsen-Jensen. Qualitative analysis of concurrent mean-payoff games. Information and Computation, 242:2-24, 2015. Google Scholar
  23. T. Chen, V. Forejt, M. Kwiatkowska, D. Parker, and A. Simaitis. Automatic Verification of Competitive Stochastic Systems. In Proc. of Tools and Algorithms for the Construction and Analysis of Systems TACAS, volume 7214 of LNCS, pages 315-330, 2012. Google Scholar
  24. T. Chen, V. Forejt, M. Kwiatkowska, D. Parker, and A. Simaitis. Automatic verification of competitive stochastic systems. Formal Methods in System Design, 43(1):61-92, 2013. Google Scholar
  25. T. Chen, V. Forejt, M. Kwiatkowska, D. Parker, and A. Simaitis. PRISM-games: A Model Checker for Stochastic Multi-Player Games. In Proc. of Tools and Algorithms for the Construction and Analysis of Systems TACAS, volume 7795 of LNCS, pages 185-191, 2013. Google Scholar
  26. Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, Aistis Simaitis, and Clemens Wiltsche. On Stochastic Games with Multiple Objectives. In Proc. of Mathematical Foundations of Computer Science MFCS, pages 266-277, 2013. Google Scholar
  27. Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, Aistis Simaitis, Ashutosh Trivedi, and Michael Ummels. Playing Stochastic Games Precisely. In Proc. of Concurrency Theory CONCUR, volume 7454 of LNCS, pages 348-363. 2012. Google Scholar
  28. Taolue Chen, Ernst Moritz Hahn, Tingting Han, Marta Kwiatkowska, Hongyang Qu, and Lijun Zhang. Model repair for Markov decision processes. In Proc. 7th Int. Symp. Theoretical Aspects of Software Engineering (TASE'13), pages 85-92. IEEE Computer Society Press, 2013. Google Scholar
  29. Taolue Chen, Marta Z. Kwiatkowska, Aistis Simaitis, and Clemens Wiltsche. Synthesis for Multi-objective Stochastic Games: An Application to Autonomous Urban Driving. In Proc. of Quantitative Evaluation of Systems QEST, pages 322-337, 2013. Google Scholar
  30. Anne Condon. The Complexity of Stochastic Games. Information and Computation, 96:203-224, 1992. Google Scholar
  31. C. Courcoubetis and M. Yannakakis. Verifying temporal properties of finite state probabilistic programs. In Proc. 29th Annual Symp. Foundations of Computer Science (FOCS'88), pages 338-345. IEEE Computer Society Press, 1988. Google Scholar
  32. F. Dannenberg, M. Kwiatkowska, C. Thachuk, and A. J. Turberfield. Dna walker circuits: Computational potential, design and verification. Natural Computing, 14(2):195-211, 2015. Google Scholar
  33. L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker, and R. Segala. Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation. In S. Graf and M. Schwartzbach, editors, Proc. 6th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00), volume 1785 of LNCS, pages 395-410. Springer, 2000. Google Scholar
  34. C. Dehnert, S. Junges, N. Jansen, F. Corzilius, M. Volk, H. Bruintjes, J-P. Katoen, and E. Ábrahám. PROPhESY: A PRObabilistic ParamEter SYnthesis tool. In Proc. 27th Int. Conf. Computer Aided Verification (CAV'15), volume 9206 of LNCS, pages 214-231. Springer, 2015. Google Scholar
  35. T. Deshpande, P. Katsaros, S.A. Smolka, and S.D. Stoller. Stochastic Game-Based Analysis of the DNS Bandwidth Amplification Attack Using Probabilistic Model Checking. In Proc. of European Dependable Computing Conference EDCC, pages 226-237, 2014. Google Scholar
  36. M. Diciolla, C. H. P. Kim, M. Kwiatkowska, and A. Mereacre. Synthesising optimal timing delays for timed I/O automata. In Proc. 14th International Conference on Embedded Software (EMSOFT'14). ACM, 2014. Google Scholar
  37. M. Duflot, M. Kwiatkowska, G. Norman, and D. Parker. A formal analysis of Bluetooth device discovery. Int. Journal on Software Tools for Technology Transfer, 8(6):621-632, 2006. Google Scholar
  38. K. Etessami, M. Kwiatkowska, M. Vardi, and M. Yannakakis. Multi-objective model checking of Markov decision processes. Logical Methods in Computer Science, 4(4):1-21, 2008. Google Scholar
  39. R. Falcone and C. Castelfranchi. Social trust: A cognitive approach. In Trust and Deception in Virtual Societies, pages 55-90. Kluwer, 2001. Google Scholar
  40. Lu Feng, Clemens Wiltsche, Laura Humphrey, and Ufuk Topcu. Controller Synthesis for Autonomous Systems Interacting with Human Operators. In Proc. of Int. Conf. on Cyber-Physical Systems ICCPS, pages 70-79, 2015. Google Scholar
  41. V. Forejt, M. Kwiatkowska, G. Norman, and D. Parker. Automated Verification Techniques for Probabilistic Systems. In Proc. of Formal Methods for Eternal Networked Software System SFM, volume 6659 of LNCS, pages 53-113, 2011. Google Scholar
  42. V. Forejt, M. Kwiatkowska, G. Norman, D. Parker, and H. Qu. Quantitative multi-objective verification for probabilistic systems. In P. Abdulla and K. Leino, editors, Proc. 17th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11), volume 6605 of LNCS, pages 112-127. Springer, 2011. Google Scholar
  43. D. Gillette. Stochastic games with zero stop probabilities. Contributions to the Theory of Games, 39:179-187, 1957. Google Scholar
  44. T.J. Glazier, J. Camara, B. Schmerl, and D. Garlan. Analyzing Resilience Properties of Different Topologies of Collective Adaptive Systems. In Proc. of Self-Adaptive and Self-Organizing Systems Workshops SASOW, pages 55-60, 2015. Google Scholar
  45. J. Heath, M. Kwiatkowska, G. Norman, D. Parker, and O. Tymchyshyn. Probabilistic model checking of complex biological pathways. Theoretical Computer Science, 319(3):239-257, 2008. Google Scholar
  46. X. Huang and M. Kwiatkowska. Reasoning about cognitive trust in stochastic multiagent systems. Technical Report CS-RR-16-02, Department of Computer Science, University of Oxford, 2016. Google Scholar
  47. M. Kattenbelt, M. Kwiatkowska, G. Norman, and D. Parker. Abstraction refinement for probabilistic software. In N. Jones and M. Muller-Olm, editors, Proc. 10th Int. Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI'09), volume 5403 of LNCS, pages 182-197. Springer, 2009. Google Scholar
  48. M. Kwiatkowska. Model checking for probability and time: From theory to practice. In Proc. 18th Annual IEEE Symp. Logic in Computer Science (LICS'03), pages 351-360. IEEE Computer Society Press, 2003. Invited Paper. Google Scholar
  49. M. Kwiatkowska, G. Norman, and D. Parker. PRISM: Probabilistic symbolic model checker. In T. Field, P. Harrison, J. Bradley, and U. Harder, editors, Proc. 12th Int. Conf. Modelling Techniques and Tools for Computer Performance Evaluation (TOOLS'02), volume 2324 of LNCS, pages 200-204. Springer, 2002. Google Scholar
  50. M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic symbolic model checking with PRISM: A hybrid approach. International Journal on Software Tools for Technology Transfer (STTT), 6(2):128-142, 2004. Google Scholar
  51. M. Kwiatkowska, G. Norman, and D. Parker. PRISM 4.0: Verification of probabilistic real-time systems. In G. Gopalakrishnan and S. Qadeer, editors, Proc. 23rd Int. Conf. Computer Aided Verification (CAV'11), volume 6806 of LNCS, pages 585-591. Springer, 2011. Google Scholar
  52. M. Kwiatkowska, G. Norman, and D. Parker. PRISM 4.0: Verification of Probabilistic Real-time Systems. In Proc. of Computer Aided Verification CAV, volume 6806 of LNCS, pages 585-591, 2011. Google Scholar
  53. M. Kwiatkowska, G. Norman, and R. Segala. Automated verification of a randomized distributed consensus protocol using Cadence SMV and PRISM. In G. Berry, H. Comon, and A. Finkel, editors, Proc. 13th Int. Conf. Computer Aided Verification (CAV'01), volume 2102 of LNCS, pages 194-206. Springer, 2001. Google Scholar
  54. M. Kwiatkowska, D. Parker, and C. Wiltsche. PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games. In Proc. of Tools and Algorithms for the Construction and Analysis of Systems TACAS, 2016. to appear. Google Scholar
  55. Marta Kwiatkowska, Alexandru Mereacre, Nicola Paoletti, and Andrea Patanè. Synthesising robust and optimal parameters for cardiac pacemakers using symbolic and evolutionary computation techniques. In Proceedings of the 4th International Workshop on Hybrid Systems and Biology (HSB 2015), volume 9271 of LNCS/LNBI, pages 119-140. Springer, 2015. Google Scholar
  56. Marta Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu. Compositional probabilistic verification through multi-objective model checking. Information and Computation, 232:38-65, 2013. Google Scholar
  57. M. Lakin, D. Parker, L. Cardelli, M. Kwiatkowska, and A. Phillips. Design and analysis of DNA strand displacement devices using probabilistic model checking. Journal of the Royal Society Interface, 9(72):1470-1485, 2012. Google Scholar
  58. Thomas M. Liggett and Steven A. Lippman. Stochastic Games with Perfect Information and Time Average Payoff. SIAM Review, 11(4):604-607, 1969. Google Scholar
  59. G. Norman, D. Parker, M. Kwiatkowska, and S. Shukla. Evaluating the reliability of NAND multiplexing with PRISM. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 24(10):1629-1637, 2005. Google Scholar
  60. D. Parker. Implementation of Symbolic Model Checking for Probabilistic Systems. PhD thesis, University of Birmingham, 2002. Google Scholar
  61. PRISM-games website. URL: http://www.prismmodelchecker.org/games/.
  62. Dorsa Sadigh, Katherine Driggs-Campbell, Alberto Puggelli, Wenchao Li, Victor Shia, Ruzena Bajcsy, Alberto L. Sangiovanni-Vincentelli, S. Shankar Sastry, and Sanjit A. Seshia. Data-driven probabilistic modeling and verification of human driver behavior. In Formal Verification and Modeling in Human-Machine Systems, AAAI Spring Symposium, 2014. Google Scholar
  63. R. Segala. Modelling and Verification of Randomized Distributed Real Time Systems. PhD thesis, Massachusetts Institute of Technology, 1995. Google Scholar
  64. L. S. Shapley. Stochastic games. In National Academy of Sciences, pages 1095-1100, 1953. Google Scholar
  65. V. Shmatikov. Probabilistic analysis of anonymity. In Proc. 15th IEEE Computer Security Foundations Workshop (CSFW'02), pages 119-128. IEEE Computer Society Press, 2002. Google Scholar
  66. A. Simaitis. Automatic Verification of Competitive Stochastic Systems. PhD thesis, Department of Computer Science, University of Oxford, 2014. Google Scholar
  67. M. Svorenova and M. Kwiatkowska. Quantitative verification and strategy synthesis for stochastic games. European Journal of Control, 2016. To appear. Google Scholar
  68. M. Ujma. On Verification and Controller Synthesis for Probabilistic Systems at Runtime. PhD thesis, University of Oxford, 2015. Google Scholar
  69. Moshe Y. Vardi. Automatic verification of probabilistic concurrent finite state programs. Foundations of Computer Science, IEEE Annual Symposium on, 0:327-338, 1985. Google Scholar
  70. C. Wiltsche. Assume-Guarantee Strategy Synthesis for Stochastic Games. PhD thesis, Department of Computer Science, University of Oxford, 2015. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact