MultiGain

MultiGain is a tool built on top of the PRISM model checker. It provides the ability to:

Verify multi-objective mean payoff querieas in Markov decision processes, i.e. check whether there is a strategy satisfying several mean-payoff constraints at the same time. Optionally, one can ask for the existence of a memoryless strategy
Generate the witnessing strategy for the above
Perform simulations under the strategy, and create the Markov chain which is a product of the Markov decision process and the strategy

Note that MultiGain requires Java 7.

Download

This version has several minor bugs fixed.
Windows (32 bit)
Linux (64 bit)
Source-based installation

This version offers simplified steps for including Gurobi support.
Windows (32 bit)
Linux (64 bit)
Source-based installation

Download an archive with source files, unpack, and follow the instructions provided in README.txt