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

DOI10.1007/978-3-030-72016-2_13MaRDI QIDQ2044201zbMATH OpenOpenAlexFDO

Authors Tim Quatmann, Joost-Pieter Katoen

Publication date 4 August 2021

Copyright license Creative Commons Attribution 4.0 International

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

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)

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.

Recommendations

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

Cites work

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