Cargando…

Stochastic Games with Lexicographic Reachability-Safety Objectives

We study turn-based stochastic zero-sum games with lexicographic preferences over reachability and safety objectives. Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as angelic and demonic non-determinis...

Descripción completa

Detalles Bibliográficos
Autores principales: Chatterjee, Krishnendu, Katoen, Joost-Pieter, Weininger, Maximilian, Winkler, Tobias
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363229/
http://dx.doi.org/10.1007/978-3-030-53291-8_21
_version_ 1783559627941609472
author Chatterjee, Krishnendu
Katoen, Joost-Pieter
Weininger, Maximilian
Winkler, Tobias
author_facet Chatterjee, Krishnendu
Katoen, Joost-Pieter
Weininger, Maximilian
Winkler, Tobias
author_sort Chatterjee, Krishnendu
collection PubMed
description We study turn-based stochastic zero-sum games with lexicographic preferences over reachability and safety objectives. Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as angelic and demonic non-determinism. Lexicographic order allows to consider multiple objectives with a strict preference order over the satisfaction of the objectives. To the best of our knowledge, stochastic games with lexicographic objectives have not been studied before. We establish determinacy of such games and present strategy and computational complexity results. For strategy complexity, we show that lexicographically optimal strategies exist that are deterministic and memory is only required to remember the already satisfied and violated objectives. For a constant number of objectives, we show that the relevant decision problem is in [Formula: see text], matching the current known bound for single objectives; and in general the decision problem is [Formula: see text]-hard and can be solved in [Formula: see text]. We present an algorithm that computes the lexicographically optimal strategies via a reduction to computation of optimal strategies in a sequence of single-objectives games. We have implemented our algorithm and report experimental results on various case studies.
format Online
Article
Text
id pubmed-7363229
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73632292020-07-16 Stochastic Games with Lexicographic Reachability-Safety Objectives Chatterjee, Krishnendu Katoen, Joost-Pieter Weininger, Maximilian Winkler, Tobias Computer Aided Verification Article We study turn-based stochastic zero-sum games with lexicographic preferences over reachability and safety objectives. Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as angelic and demonic non-determinism. Lexicographic order allows to consider multiple objectives with a strict preference order over the satisfaction of the objectives. To the best of our knowledge, stochastic games with lexicographic objectives have not been studied before. We establish determinacy of such games and present strategy and computational complexity results. For strategy complexity, we show that lexicographically optimal strategies exist that are deterministic and memory is only required to remember the already satisfied and violated objectives. For a constant number of objectives, we show that the relevant decision problem is in [Formula: see text], matching the current known bound for single objectives; and in general the decision problem is [Formula: see text]-hard and can be solved in [Formula: see text]. We present an algorithm that computes the lexicographically optimal strategies via a reduction to computation of optimal strategies in a sequence of single-objectives games. We have implemented our algorithm and report experimental results on various case studies. 2020-06-16 /pmc/articles/PMC7363229/ http://dx.doi.org/10.1007/978-3-030-53291-8_21 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Chatterjee, Krishnendu
Katoen, Joost-Pieter
Weininger, Maximilian
Winkler, Tobias
Stochastic Games with Lexicographic Reachability-Safety Objectives
title Stochastic Games with Lexicographic Reachability-Safety Objectives
title_full Stochastic Games with Lexicographic Reachability-Safety Objectives
title_fullStr Stochastic Games with Lexicographic Reachability-Safety Objectives
title_full_unstemmed Stochastic Games with Lexicographic Reachability-Safety Objectives
title_short Stochastic Games with Lexicographic Reachability-Safety Objectives
title_sort stochastic games with lexicographic reachability-safety objectives
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363229/
http://dx.doi.org/10.1007/978-3-030-53291-8_21
work_keys_str_mv AT chatterjeekrishnendu stochasticgameswithlexicographicreachabilitysafetyobjectives
AT katoenjoostpieter stochasticgameswithlexicographicreachabilitysafetyobjectives
AT weiningermaximilian stochasticgameswithlexicographicreachabilitysafetyobjectives
AT winklertobias stochasticgameswithlexicographicreachabilitysafetyobjectives