DROPS

Document

DOI: 10.4230/LIPIcs.ICALP.2017.121

Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes

Authors: Raphaël Berthon, Mickael Randour, and Jean-François Raskin

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract

The beyond worst-case synthesis problem was introduced recently by Bruyère et al. [BFRR14]: it aims at building system controllers that provide strict worst-case performance guarantees against an antagonistic environment while ensuring higher expected performance against a stochastic model of the environment. Our work extends the framework of [Bruyère/Filiot/Randour/Raskin, STACS 2014] and follow-up papers, which focused on quantitative objectives, by addressing the case of omega-regular conditions encoded as parity objectives, a natural way to represent functional requirements of systems. We build strategies that satisfy a main parity objective on all plays, while ensuring a secondary one with sufficient probability. This setting raises new challenges in comparison to quantitative objectives, as one cannot easily mix different strategies without endangering the functional properties of the system. We establish that, for all variants of this problem, deciding the existence of a strategy lies in NP and in coNP, the same complexity class as classical parity games. Hence, our framework provides additional modeling power while staying in the same complexity class.

Cite as

Raphaël Berthon, Mickael Randour, and Jean-François Raskin. Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 121:1-121:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{berthon_et_al:LIPIcs.ICALP.2017.121,
  author =	{Berthon, Rapha\"{e}l and Randour, Mickael and Raskin, Jean-Fran\c{c}ois},
  title =	{{Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{121:1--121:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.121},
  URN =		{urn:nbn:de:0030-drops-74360},
  doi =		{10.4230/LIPIcs.ICALP.2017.121},
  annote =	{Keywords: Markov decision processes, parity objectives, beyond worst-case synthesis}
}

Search Results

Documents authored by Berthon, Raphaël

Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes

Abstract

Cite as

Thanks for your feedback!

Could not send message