Simple Strategies in Multi-Objective MDPs
Ontology highlight
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.
SUBMITTER: Biere A
PROVIDER: S-EPMC7439746 | biostudies-literature | 2020 Mar
REPOSITORIES: biostudies-literature
ACCESS DATA