Stochastic games with lexicographic reachability-safety objectives

DOI10.1007/978-3-030-53291-8_21zbMATH Open1478.68151arXiv2005.04018OpenAlexW3046820103MaRDI QIDQ2226751FDOQ2226751

Tobias Winkler, Joost-Pieter Katoen, Krishnendu Chatterjee, Maximilian Weininger

Publication date: 9 February 2021

Abstract: 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 NP $cap$ coNP, matching the current known bound for single objectives; and in general the decision problem is PSPACE-hard and can be solved in NEXPTIME $cap$ coNEXPTIME. 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.

Full work available at URL: https://arxiv.org/abs/2005.04018

Recommendations

• On stochastic games with multiple objectives
• Perfect-information stochastic games with generalized mean-payoff objectives
• Stochastic Games with Finitary Objectives
• Strategy improvement for concurrent reachability and turn-based stochastic safety games
• A Survey of Stochastic Games with Limsup and Liminf Objectives

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60) Stochastic games, stochastic differential games (91A15) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (15)

• Automata-based controller synthesis for stochastic systems: a game framework via approximate probabilistic relations
• Comparison of algorithms for simple stochastic games
• Symbolic verification and strategy synthesis for turn-based stochastic games
• A dynamic game approach to distributionally robust safety specifications for stochastic systems
• Multi-weighted reachability games
• Title not available (Why is that?)
• Composition of stochastic services for LTL\(_f\) goal specifications
• Preface of the special issue on the conference on computer-aided verification 2020 and 2021
• Stochastic games with lexicographic objectives
• Stochastic games with disjunctions of multiple objectives
• On equilibria in quantitative games with reachability/safety objectives
• Computing lexicographically safe Nash equilibria in finite two-person games with tight game forms given by oracles
• Model-Free Reinforcement Learning for Lexicographic Omega-Regular Objectives
• Synthesising Succinct Strategies in Safety and Reachability Games
• Multi-agent verification and control with probabilistic model checking

This page was built for publication: Stochastic games with lexicographic reachability-safety objectives

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2226751)