MULTIGAIN 2.0：面向多重平均收益、LTL 与稳态约束的 MDP 控制器综合
人工智能
2024-05-03 v2 计算机科学中的逻辑
摘要
我们提出 MULTIGAIN 2.0，这是对控制器综合工具 MULTIGAIN 的重大扩展，构建于概率模型检测器 PRISM 之上。该新版本扩展了 MULTIGAIN 的多目标能力，允许对具有多维长期平均奖励结构、稳态约束和线性时序逻辑属性的概率系统进行形式化验证与控制器综合。此外，MULTIGAIN 2.0 可修改底层线性规划以防止无界内存及其他不直观的解，并在二维与三维情形下可视化帕累托曲线，以促进多目标场景中的权衡分析。
引用
@article{arxiv.2305.16752,
title = {MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints},
author = {Severin Bals and Alexandros Evangelidis and Jan Křetínský and Jakob Waibel},
journal= {arXiv preprint arXiv:2305.16752},
year = {2024}
}