License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2016.4
URN: urn:nbn:de:0030-drops-62285
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6228/
Go to the corresponding LIPIcs Volume Portal

Kwiatkowska, Marta Z.

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

pdf-format:
LIPIcs-ICALP-2016-4.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{kwiatkowska:LIPIcs:2016:6228,
  author =	{Marta Z. Kwiatkowska},
  title =	{{Model Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice (Invited Talk)}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{4:1--4:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Ioannis Chatzigiannakis and Michael Mitzenmacher and Yuval Rabani and Davide Sangiorgi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6228},
  URN =		{urn:nbn:de:0030-drops-62285},
  doi =		{10.4230/LIPIcs.ICALP.2016.4},
  annote =	{Keywords: Quantitative verification, Stochastic games, Temporal logic, Model checking, Strategy synthesis}
}

Keywords: Quantitative verification, Stochastic games, Temporal logic, Model checking, Strategy synthesis
Collection: 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)
Issue Date: 2016
Date of publication: 23.08.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI