Finite-memory strategy synthesis for robust multidimensional mean-payoff objectives

DOI10.1145/2603088.2603096MaRDI QIDQ4635664zbMATH OpenOpenAlexFDO

Authors Yaron Velner

Publication date 23 April 2018

Published in Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (Search for Journal in Brave)

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

zbMATH Keywords

mean-payoff gamesquantitative synthesismultidimensional quantitative games on graphs

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) 2-person games (91A05) Games involving graphs (91A43) Decidability (number-theoretic aspects) (11U05)

Abstract: Two-player games on graphs provide the mathematical foundation for the study of reactive systems. In the quantitative framework, an objective assigns a value to every play, and the goal of player 1 is to minimize the value of the objective. In this framework, there are two relevant synthesis problems to consider: the quantitative analysis problem is to compute the minimal (or infimum) value that player 1 can assure, and the boolean analysis problem asks whether player 1 can assure that the value of the objective is at most $u$ (for a given threshold $u$). Mean-payoff expression games are played on a multidimensional weighted graph. An atomic mean-payoff expression objective is the mean-payoff value (the long-run average weight) of a certain dimension, and the class of mean-payoff expressions is the closure of atomic mean-payoff expressions under the algebraic operations of $MAX,MIN$, numerical complement and $SUM$. In this work, we study for the first time the strategy synthesis problems for games with robust quantitative objectives, namely, games with mean-payoff expression objectives. While in general, optimal strategies for these games require infinite-memory, in synthesis we are typically interested in the construction of a finite-state system. Hence, we consider games in which player 1 is restricted to finite-memory strategies, and our main contribution is as follows. We prove that for mean-payoff expressions, the quantitative analysis problem is computable, and the boolean analysis problem is inter-reducible with Hilbert's tenth problem over rationals --- a fundamental long-standing open problem in computer science and mathematics.

Recommendations

• Multi-objective Robust Strategy Synthesis for Interval Markov Decision Processes
• Finite-memory strategies in POMDPs with long-run average objectives
• Efficient Strategy Synthesis for MDPs With Resource Constraints
• Strategy synthesis for stochastic games with multiple long-run objectives
• Compositional strategy synthesis for stochastic games with multiple objectives
• Efficient strategy iteration for mean payoff in Markov decision processes
• Robust optimal strategies in Markov decision problems
• Finite-Memory Suboptimal Design for Partially Observed Markov Decision Processes
• Optimal Strategy Synthesis in Stochastic Müller Games
• Multidimensional beyond worst-case and almost-sure problems for mean-payoff objectives

Cited in

(3)

• Multi-objective Robust Strategy Synthesis for Interval Markov Decision Processes
• Robust multidimensional mean-payoff games are undecidable
• Compositional strategy synthesis for stochastic games with multiple objectives

This page was built for publication: Finite-memory strategy synthesis for robust multidimensional mean-payoff objectives

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