Multi-objective Optimization of Long-run Average and Total Rewards

TL;DR

This paper introduces an efficient method for multi-objective model checking of long-run average and total rewards in Markov automata, improving performance over existing techniques and applicable to both MDPs and continuous-time models.

Contribution

It generalizes existing approaches for total rewards to handle combined long-run and total reward objectives in Markov automata, enhancing efficiency and applicability.

Findings

Encouraging experimental results on Storm model checker

Significant performance improvements over linear programming methods

Effective handling of combined long-run and total reward objectives

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.