Various algorithms and tools for the formal verification of systems with respect to their quantitative behavior have been developed in the past decades. Many of these techniques inherently support the automated synthesis of strategies that guarantee the satisfaction of performance or reliability constraints by resolving controllable nondeterministic choices in an adequate way. More recently, such techniques have been further developed towards the analysis or strategy synthesis under multiple cost and utility constraints.

This article deals with Markov decision processes (MDPs) for modeling systems and their environment and provides an overview of recent directions for different types of synthesis problems in MDPs that aim to achieve an acceptable cost-utility tradeoff.