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.

翻译：本文介绍MULTIGAIN 2.0——基于概率模型检测器PRISM构建的控制器综合工具MULTIGAIN的重大扩展版本。该新版本通过支持具有多维长期平均回报结构、稳态约束及线性时序逻辑属性的概率系统的形式化验证与控制器综合，扩展了MULTIGAIN的多目标处理能力。此外，MULTIGAIN 2.0可对底层线性规划进行修改以避免无界内存及其他非直观解，并在二维与三维情形下可视化帕累托曲线，以促进多目标场景中的权衡分析。