Simple Strategies in Multi-Objective MDPs

Lecture notes in computer science, pp. 346–364

Abstract

We consider the verification of multiple expected reward objectives at once on Markov decision processes (MDPs). This enables a trade-off analysis among multiple objectives by obtaining a Pareto front. We focus on strategies that are easy to employ and implement. That is, strategies that are pure (no randomization) and have bounded memory. We show that checking whether a point is achievable by a pure stationary strategy is NP-complete, even for two objectives, and we provide an MILP encoding to solve the corresponding problem. The bounded memory case is treated by a product construction. Experimental results using S torm and G urobi show the feasibility of our algorithms.

Authors 4

1. Florent Delgrange Aachen

   University of Mons · RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

   UMONS – Université de Mons, Mons, Belgium

2. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

3. Tim Quatmann corresponding Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

4. Mickaël Randour

   University of Mons

   Affiliation as printed

   UMONS – Université de Mons, Mons, Belgium