MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints
This work provides a tool for researchers and engineers in formal verification and control systems, but it is incremental as it builds upon existing MULTIGAIN capabilities.
The authors tackled the problem of controller synthesis for probabilistic systems by extending MULTIGAIN to handle multi-dimensional long-run average rewards, steady-state constraints, and LTL properties, resulting in a tool that prevents unbounded-memory solutions and visualizes Pareto curves for trade-off analysis.
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.