Strategy synthesis for multi-dimensional quantitative objectives

DOI10.1007/978-3-642-32940-1_10zbMATH Open1360.68208arXiv1201.5073OpenAlexW2785504350MaRDI QIDQ2249657FDOQ2249657

Mickael Randour, Jean-François Raskin, Krishnendu Chatterjee

Publication date: 3 July 2014

Published in: Acta Informatica, Lecture Notes in Computer Science (Search for Journal in Brave)

Abstract: Multi-dimensional mean-payoff and energy games provide the mathematical foundation for the quantitative study of reactive systems, and play a central role in the emerging quantitative theory of verification and synthesis. In this work, we study the strategy synthesis problem for games with such multi-dimensional objectives along with a parity condition, a canonical way to express $omega$-regular conditions. While in general, the winning strategies in such games may require infinite memory, for synthesis the most relevant problem is the construction of a finite-memory winning strategy (if one exists). Our main contributions are as follows. First, we show a tight exponential bound (matching upper and lower bounds) on the memory required for finite-memory winning strategies in both multi-dimensional mean-payoff and energy games along with parity objectives. This significantly improves the triple exponential upper bound for multi energy games (without parity) that could be derived from results in literature for games on VASS (vector addition systems with states). Second, we present an optimal symbolic and incremental algorithm to compute a finite-memory winning strategy (if one exists) in such games. Finally, we give a complete characterization of when finite memory of strategies can be traded off for randomness. In particular, we show that for one-dimension mean-payoff parity games, randomized memoryless strategies are as powerful as their pure finite-memory counterparts.

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

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Applications of game theory (91A80) Games involving graphs (91A43) Distributed systems (68M14) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The complexity of mean payoff games on graphs
• Alternating-time temporal logic
• Borel determinacy
• The determinacy of Blackwell games
• Simulation distances
• Automata, logics, and infinite games. A guide to current research
• Supervisory Control of a Class of Discrete Event Processes
• The covering and boundedness problems for vector addition systems
• Positional strategies for mean payoff games
• Synthesizing robust systems
• Antichain Algorithms for Finite Automata
• When Simulation Meets Antichains
• Better Quality in Synthesis through Quantitative Objectives
• Antichains: A New Algorithm for Checking Universality of Finite Automata
• Infinite games on finitely coloured graphs with applications to automata on infinite trees
• Generalized mean-payoff and energy games
• Infinite Runs in Weighted Timed Automata with Energy Constraints
• A multiparameter analysis of the boundedness problem for vector addition systems
• Bounds on Positive Integral Solutions of Linear Diophantine Equations
• Quantitative languages
• Energy Games in Multiweighted Automata
• Fair simulation
• Measuring Permissiveness in Parity Games: Mean-Payoff Parity Games Revisited
• Permissive strategies: from parity games to safety games
• Strategy synthesis for multi-dimensional quantitative objectives
• Synthesis from LTL Specifications with Mean-Payoff Objectives
• Reachability Games on Extended Vector Addition Systems with States
• Church Synthesis Problem for Noisy Input
• Energy Parity Games
• Energy and Mean-Payoff Parity Markov Decision Processes

Cited In (33)

• Title not available (Why is that?)
• Better Quality in Synthesis through Quantitative Objectives
• Deciding Parity Games in Quasi-polynomial Time
• Title not available (Why is that?)
• Synthesis for Multi-weighted Games with Branching-Time Winning Conditions
• Non-deterministic weighted automata evaluated over Markov chains
• Average-energy games
• Percentile queries in multi-dimensional Markov decision processes
• Playing with Repetitions in Data Words Using Energy Games
• On Values of Games
• Fixed-Dimensional Energy Games are in Pseudo-Polynomial Time
• Strategy synthesis for multi-dimensional quantitative objectives
• Compositional strategy synthesis for stochastic games with multiple objectives
• Looking at mean-payoff and total-payoff through windows
• The complexity of multi-mean-payoff and multi-energy games
• Bounding Average-Energy Games
• Multi-weighted reachability games
• Title not available (Why is that?)
• Title not available (Why is that?)
• Graph Games and Reactive Synthesis
• Safraless LTL synthesis considering maximal realizability
• Verification of multiplayer stochastic games via abstract dependency graphs
• Title not available (Why is that?)
• Reachability games with relaxed energy constraints
• Extending Finite-Memory Determinacy by Boolean Combination of Winning Conditions
• Different strokes in randomised strategies: revisiting Kuhn's theorem under finite-memory assumptions
• Title not available (Why is that?)
• Title not available (Why is that?)
• Model checking and synthesis for branching multi-weighted logics
• Efficient Algorithms for Omega-Regular Energy Games
• Non-deterministic Weighted Automata on Random Words
• Meet your expectations with guarantees: beyond worst-case synthesis in quantitative games
• Title not available (Why is that?)

Uses Software

• Antichains

This page was built for publication: Strategy synthesis for multi-dimensional quantitative objectives

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