# MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints

arXiv: https://arxiv.org/abs/2305.16752 · HTML: https://mlsanity.com/paper/2305.16752/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 5 of its 17 references that are in the map.
- First posted on arXiv 26 May 2023.

## Builds on (most cited first, 5 of 5)

- [Probabilistic Motion Planning under Temporal Tasks and Soft Constraints](https://mlsanity.com/paper/1706.05209/) (2017)
- [MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives](https://mlsanity.com/paper/1501.03093/) (2015)
- [Multi-objective Optimization of Long-run Average and Total Rewards](https://mlsanity.com/paper/2010.13566/) (2020)
- [LTL-Constrained Steady-State Policy Synthesis](https://mlsanity.com/paper/2105.14894/) (2021)
- [Controller Synthesis for Omega-Regular and Steady-State Specifications](https://mlsanity.com/paper/2106.02951/) (2021)

## Built on by (most cited first, 1 of 1)

- [Accelerating Policy Synthesis in Large-Scale MDPs via Hierarchical Adaptive Refinement](https://mlsanity.com/paper/2506.17792/) (2025)

## Abstract (arXiv)

We present MULTIGAIN 2.0, a major extension to the controller synthesis tool MULTIGAIN, built on top of the probabilistic model checker PRISM. This new version extends MULTIGAIN's multi-objective capabilities, by allowing for the formal verification and synthesis of controllers for probabilistic systems with multi-dimensional long-run average reward structures, steady-state constraints, and linear temporal logic properties. Additionally, MULTIGAIN 2.0 can modify the underlying linear program to prevent unbounded-memory and other unintuitive solutions and visualizes Pareto curves, in the two- and three-dimensional cases, to facilitate trade-off analysis in multi-objective scenarios.