  Multi-objective probabilistic model checking provides a way to verify
several, possibly conflicting, quantitative properties of a stochastic system.
It has useful applications in controller synthesis and compositional
probabilistic verification. However, existing methods are based on linear
programming, which limits the scale of systems that can be analysed and makes
verification of time-bounded properties very difficult. We present a novel
approach that addresses both of these shortcomings, based on the generation of
successive approximations of the Pareto curve for a multi-objective model
checking problem. We illustrate dramatic improvements in efficiency on a large
set of benchmarks and show how the ability to visualise Pareto curves
significantly enhances the quality of results obtained from current
probabilistic verification tools.
