MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints
International Conference on Hybrid Systems: Computation and Control(2023)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要