Simple Strategies in Multi-Objective MDPs
Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann, Mickaël Randour
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.
Topics & Concepts
Computer scienceBounded functionMathematical optimizationSimple (philosophy)Markov decision processFocus (optics)Encoding (memory)Pareto principleProduct (mathematics)Point (geometry)Markov processArtificial intelligenceMathematicsStatisticsOpticsMathematical analysisEpistemologyPhilosophyGeometryPhysicsFormal Methods in VerificationReinforcement Learning in RoboticsReal-Time Systems Scheduling