  We consider Markov decision processes (MDPs) in which the transition
probabilities and rewards belong to an uncertainty set parametrized by a
collection of random variables. The probability distributions for these random
parameters are unknown. The problem is to compute the probability to satisfy a
temporal logic specification within any MDP that corresponds to a sample from
these unknown distributions. In general, this problem is undecidable, and we
resort to techniques from so-called scenario optimization. Based on a finite
number of samples of the uncertain parameters, each of which induces an MDP,
the proposed method estimates the probability of satisfying the specification
by solving a finite-dimensional convex optimization problem. The number of
samples required to obtain a high confidence on this estimate is independent
from the number of states and the number of random parameters. Experiments on a
large set of benchmarks show that a few thousand samples suffice to obtain
high-quality confidence bounds with a high probability.
