  Markov decision processes (MDPs) provide a fundamental model for sequential
decision making under process uncertainty. A classical synthesis task is to
compute for a given MDP a winning policy that achieves a desired specification.
However, at design time, one typically needs to consider a family of MDPs
modelling various system variations. For a given family, we study synthesising
(1) the subset of MDPs where a winning policy exists and (2) a preferably small
number of winning policies that together cover this subset. We introduce policy
trees that concisely capture the synthesis result. The key ingredient for
synthesising policy trees is a recursive application of a game-based
abstraction. We combine this abstraction with an efficient refinement procedure
and a post-processing step. An extensive empirical evaluation demonstrates
superior scalability of our approach compared to naive baselines. For one of
the benchmarks, we find 246 winning policies covering 94 million MDPs. Our
algorithm requires less than 30 minutes, whereas the naive baseline only covers
3.7% of MDPs in 24 hours.
