面向马尔可夫决策过程中多目标 ω-正则查询的证书与证据

多目标概率模型检查是验证随机系统针对多个（可能相互冲突）性质的强大技术。为提升模型检查工具的可信度与可解释性，我们提出了面向马尔可夫决策过程中多目标 ω-正则查询的可独立验证证书与证据。对于证书，我们改进并扩展了现有用于分解最大终端组件和可达性属性的证书。随后，我们推导了用于寻找最小证据子系统的混合整数线性规划（MILP）。对于马尔可夫链和 LTL 属性的特例，我们采用无歧义的 Büchi 自动机寻找证据， resulting in an algorithm that requires single-exponential space。基于确定性自动机的现有方法在最坏情况下需要双指数空间。最后，我们考虑证书和证据的实际计算，并提供了所开发技术的实现及实验评估，展示了我们方法的有效性。