Simple Strategies in Multi-Objective MDPs
Florent Delgrange
1,2,† , Joost-Pieter Katoen
1 ,
Tim Quatmann
1 , and Mickael Randour
2
1 RWTH Aachen University, Aachen, Germany
2 UMONS – Université de Mons, Mons, Belgium
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 Storm
and Gurobi show the feasibility of our algorithms.
1 Introduction
MDPs. Markov decision processes (MDPs) [4,3] are a key model in stochastic
decision making. The classical setting involves a system subject to a stochastic
model of its environment, and the goal is to synthesize a system controller, represented as a strategy for the MDP, ensuring a given level of expected performance.
Tools such as Prism [30] and Storm [16] support MDP model checking.
Multi-objective MDPs. MDPs where the goal is to achieve a combination of objectives (rather than just one) are popular in e.g., AI [41] and verification [2]. This is
driven by applications, where controllers have to fulfill multiple, potentially conflicting objectives, requiring a trade-off analysis. This includes multi-dimension
MDPs [14,20,40,13] where weight vectors are aggregated at each step and MDPs
where the specification mixes different views (e.g., average and worst case performance) of the same weight [11,8]. With multiple objectives, optimal strategies
no longer exist in general: instead, Pareto-optimal strategies are considered. The
Pareto front, i.e., the set of non-dominated achievable value vectors is usually
non-trivial. Elaborate techniques are needed to explore it efficiently, e.g., [23,24].
Simple strategies. Another stumbling block in multi-objective MDPs is the complexity of strategies: Pareto-optimal strategies typically need both memory and
randomization. A simple conjunction of reachability objectives already requires
randomization and exponential memory (in the number of reachability sets) [40].
† currently affiliated with Vrije Universiteit Brussel.
Research partially supported by F.R.S.-FNRS Grant n
◦ F.4520.18 (ManySynth).
Mickael Randour is an F.R.S.-FNRS Research Associate.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 346–364, 2020.
https://doi.org/10.1007/978-3-030-45190-5_19
TACAS
Evaluation
Artifact
2020
Accepted
Florent Delgrange
1,2,† , Joost-Pieter Katoen
1 ,
Tim Quatmann
1 , and Mickael Randour
2
1 RWTH Aachen University, Aachen, Germany
2 UMONS – Université de Mons, Mons, Belgium
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 Storm
and Gurobi show the feasibility of our algorithms.
1 Introduction
MDPs. Markov decision processes (MDPs) [4,3] are a key model in stochastic
decision making. The classical setting involves a system subject to a stochastic
model of its environment, and the goal is to synthesize a system controller, represented as a strategy for the MDP, ensuring a given level of expected performance.
Tools such as Prism [30] and Storm [16] support MDP model checking.
Multi-objective MDPs. MDPs where the goal is to achieve a combination of objectives (rather than just one) are popular in e.g., AI [41] and verification [2]. This is
driven by applications, where controllers have to fulfill multiple, potentially conflicting objectives, requiring a trade-off analysis. This includes multi-dimension
MDPs [14,20,40,13] where weight vectors are aggregated at each step and MDPs
where the specification mixes different views (e.g., average and worst case performance) of the same weight [11,8]. With multiple objectives, optimal strategies
no longer exist in general: instead, Pareto-optimal strategies are considered. The
Pareto front, i.e., the set of non-dominated achievable value vectors is usually
non-trivial. Elaborate techniques are needed to explore it efficiently, e.g., [23,24].
Simple strategies. Another stumbling block in multi-objective MDPs is the complexity of strategies: Pareto-optimal strategies typically need both memory and
randomization. A simple conjunction of reachability objectives already requires
randomization and exponential memory (in the number of reachability sets) [40].
† currently affiliated with Vrije Universiteit Brussel.
Research partially supported by F.R.S.-FNRS Grant n
◦ F.4520.18 (ManySynth).
Mickael Randour is an F.R.S.-FNRS Research Associate.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 346–364, 2020.
https://doi.org/10.1007/978-3-030-45190-5_19
TACAS
Evaluation
Artifact
2020
Accepted