Multi-objective optimization of long-run average and total rewards

DOI10.1007/978-3-030-72016-2_13zbMATH Open1467.68094arXiv2010.13566OpenAlexW3147073715MaRDI QIDQ2044201FDOQ2044201

Authors: Tim Quatmann, Joost-Pieter Katoen 

Publication date: 4 August 2021

Abstract: This paper presents an efficient procedure for multi-objective model checking of long-run average reward (aka: mean pay-off) and total reward objectives as well as their combination. We consider this for Markov automata, a compositional model that captures both traditional Markov decision processes (MDPs) as well as a continuous-time variant thereof. The crux of our procedure is a generalization of Forejt et al.'s approach for total rewards on MDPs to arbitrary combinations of long-run and total reward objectives on Markov automata. Experiments with a prototypical implementation on top of the Storm model checker show encouraging results for both model types and indicate a substantial improved performance over existing multi-objective long-run MDP model checking based on linear programming.

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

Recommendations

• Long-Run Rewards for Markov Automata
• Markov Decision Processes with Multiple Long-Run Average Objectives
• Multi-Objective Model Checking of Markov Decision Processes

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Multi-objective and goal programming (90C29) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60) Markov and semi-Markov decision processes (90C40)

Cites Work

• Title not available (Why is that?)
• On the semantics of Markov automata
• Optimal continuous time Markov decisions
• Markov Decision Processes with Multiple Objectives
• Markov Decision Processes with Multiple Long-Run Average Objectives
• Quantitative multi-objective verification for probabilistic systems
• Trading performance for stability in Markov decision processes
• Multi-Objective Model Checking of Markov Decision Processes
• Pareto curves for probabilistic model checking
• Markov decision processes with multiple long-run average objectives
• Approximating values of generalized-reachability stochastic games
• Analysis of timed and long-run objectives for Markov automata
• A semantics for every GSPN
• Enhancement of sandwich algorithms for approximating higher-dimensional convex Pareto sets
• The 10,000 facets of MDP model checking
• Optimistic value iteration
• Sound value iteration
• Perfect-information stochastic games with generalized mean-payoff objectives
• Approximating the noninferior set in multiobjective linear programming problems
• Compositional strategy synthesis for stochastic games with multiple objectives
• Strategy synthesis for stochastic games with multiple long-run objectives
• Modelling and analysis of Markov reward automata
• Value iteration for long-run average reward in Markov decision processes
• Multi-objective optimization of long-run average and total rewards
• Multi-cost bounded tradeoff analysis in MDP
• Multi-cost bounded reachability in MDP
• Long-Run Rewards for Markov Automata
• Probabilistic Motion Planning Under Temporal Tasks and Soft Constraints
• Trade-off analysis meets probabilistic model checking
• Simple strategies in multi-objective MDPs
• Efficient strategy iteration for mean payoff in Markov decision processes
• Synthesis of Optimal Resilient Control Strategies
• Stochastic shortest paths and weight-bounded properties in Markov decision processes
• Unifying two views on multiple mean-payoff objectives in Markov decision processes
• Percentile queries in multi-dimensional Markov decision processes

Cited In (2)

• Multi-objective optimization of long-run average and total rewards
• Stochastic games with lexicographic objectives

This page was built for publication: Multi-objective optimization of long-run average and total rewards

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