In this project the multi-objective mean-payoff properties in Markov decision process are to be added into Prism, which is a probabilistic model checker. In this project the following things are done to Prism:
• Multi-objective mean-payoff properties support in Markov decision process is extended, namely the algorithm defined in  is planned to be added. This should be based on the already existing MultiGain.
• A conversion algorithm for f LT L (GU ) formulae to a MOMP, defined in .
• The (already existing) Rabinizer for converting LTL to DTGRA, be- cause it heavily intersects with the conversion algorithm for f LT L (GU ) .
 Chatterjee, Krishnendu, Zuzana Komarkova, and Jan Kretinsky. ”Uni- fying two views on multiple mean-payoff objectives in Markov deci- sion processes.” Logic in Computer Science (LICS), 2015 30th Annual ACM/IEEE Symposium on. IEEE, 2015.
 Forejt, V., J. Krcl, and J. Kretnsk. ”Controller synthesis for MDPS and frequency LTL GU (2015).” CoRR, abs/1509.04116.