Pareto Curves for Probabilistic Model Checking

[Kaustabha Ray]

Hello,

I was trying to run the code for the paper Pareto Curves for Probabilistic Model Checking available at http://www.prismmodelchecker.org/files/atva12mo/.

I was using the model http://www.prismmodelchecker.org/files/atva12mo/MDP_a2_r3_t2_full_exp.nm.php

And the property // Numerical: maximise probability of completing task 1 // with 95% of possible value for expected W1 (size of successful team) "num_task1": multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=(0.95*q1) [ F true ])

However, it shows an error that Only the C and C>=k reward operators are currently supported for multi-objective properties. Is there some other extension to be used for these kind of properties in PRISM?

Thanks