\section{Conclusions}\label{concl-sect}

\vspace*{-0.2cm}
We have presented novel techniques for multi-objective model checking of MDPs,
using a value iteration-based computation to build successive approximations of the Pareto curve.
Compared to existing approaches, this gives significant gains in efficiency and scalability,
and enables verification of time-bounded properties.
Furthermore, we showed the benefits of visualising the Pareto curve
for several probabilistic model checking case studies.
Future directions include extending our techniques
to timed probabilistic models such as CTMDPs and PTAs.

