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

TL;DR

MULTIGAIN 2.0 is an advanced controller synthesis tool that enables formal verification and multi-objective optimization for probabilistic systems with complex constraints and properties.

Contribution

It extends the capabilities of MULTIGAIN to handle multi-dimensional rewards, steady-state constraints, LTL properties, and visualizes Pareto trade-offs.

Findings

Supports multi-objective controller synthesis with complex constraints.

Visualizes Pareto curves for trade-off analysis.

Prevents unbounded-memory solutions in linear programming.

Abstract

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.