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 [1] 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 [2].

• The (already existing) Rabinizer for converting LTL to DTGRA, be- cause it heavily intersects with the conversion algorithm for f LT L (GU ) .

[1] 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.

[2] Forejt, V., J. Krcl, and J. Kretnsk. ”Controller synthesis for MDPS and frequency LTL GU (2015).” CoRR, abs/1509.04116.





  • Jan Kretinsky
  • Vojtech Forejt