  Synthesising verifiably correct controllers for dynamical systems is crucial
for safety-critical problems. To achieve this, it is important to account for
uncertainty in a robust manner, while at the same time it is often of interest
to avoid being overly conservative with the view of achieving a better cost. We
propose a method for verifiably safe policy synthesis for a class of finite
state models, under the presence of structural uncertainty. In particular, we
consider uncertain parametric Markov decision processes (upMDPs), a special
class of Markov decision processes, with parameterised transition functions,
where such parameters are drawn from a (potentially) unknown distribution. Our
framework leverages recent advancements in the so-called scenario approach
theory, where we represent the uncertainty by means of scenarios, and provide
guarantees on synthesised policies satisfying probabilistic computation tree
logic (PCTL) formulae. We consider several common benchmarks/problems and
compare our work to recent developments for verifying upMDPs.
