Simple Strategies in Multi-Objective MDPs

Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann, Mickael Randour

Onderzoeksoutput: Conference paper

48 Downloads (Pure)


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 Storm and Gurobi show the feasibility of our algorithms.
Originele taal-2English
TitelTools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I
RedacteurenArmin Biere, David Parker
Aantal pagina's19
ISBN van elektronische versie978-3-030-45190-5
ISBN van geprinte versie978-3-030-45189-9
StatusPublished - 17 apr 2020
EvenementEuropean Joint Conferences on Theory and Practice of Software: Tools and Algorithms for the Construction and Analysis of Systems - Dublin, Ireland
Duur: 25 apr 202030 apr 2020
Congresnummer: 26

Publicatie series

NaamLecture Notes in Computer Science


ConferenceEuropean Joint Conferences on Theory and Practice of Software
Verkorte titelETAPS 2020
Internet adres


Duik in de onderzoeksthema's van 'Simple Strategies in Multi-Objective MDPs'. Samen vormen ze een unieke vingerafdruk.

Citeer dit