MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives

TL;DR

MultiGain is a new tool that extends PRISM to synthesize strategies for MDPs with multiple mean-payoff objectives, enabling strategy generation, exploration, and Pareto curve approximation.

Contribution

It introduces novel algorithms for multiple mean-payoff objectives and integrates them into PRISM, including a practical algorithm for analyzing MDPs with these objectives under memoryless strategies.

Findings

Successfully generates strategies for MDPs with multiple objectives.

Provides approximate Pareto curves for two mean-payoff objectives.

Includes a practical algorithm for analysis under memoryless strategies.

Abstract

We present MultiGain, a tool to synthesize strategies for Markov decision processes (MDPs) with multiple mean-payoff objectives. Our models are described in PRISM, and our tool uses the existing interface and simulator of PRISM. Our tool extends PRISM by adding novel algorithms for multiple mean-payoff objectives, and also provides features such as (i)~generating strategies and exploring them for simulation, and checking them with respect to other properties; and (ii)~generating an approximate Pareto curve for two mean-payoff objectives. In addition, we present a new practical algorithm for the analysis of MDPs with multiple mean-payoff objectives under memoryless strategies.