策略在树上生长：MDP 族的模型检查
计算机科学中的逻辑
2024-07-18 v1
摘要
马尔可夫决策过程（MDP）为序列决策在过程不确定性下提供了基本模型。一个经典的合成任务是为给定的 MDP 计算一个实现期望规格的获胜策略。然而，在设计时期，人们通常需要考虑一族模型这些系统变体。对于给定的族，我们研究合成 (1) 存在获胜策略的 MDP 子集以及 (2) 一组最佳小数量的获胜策略，这些策略共同覆盖该子集。我们引入了策略树，以简洁地捕获合成结果。合成策略树的关键要素是递归应用一种基于游戏的抽象。我们将该抽象与一种高效的细化程序和后处理步骤相结合。广泛的实证评估表明，我们的方法在可扩展性方面优于天真的基准方法。对于其中一个基准，我们发现 246 个获胜策略覆盖了 9400 万个 MDP。我们的算法在不到 30 分钟内即可完成，而天然的基准方法则在 24 小时内仅覆盖 3.7% 的 MDP。
引用
@article{arxiv.2407.12552,
title = {Policies Grow on Trees: Model Checking Families of MDPs},
author = {Roman Andriushchenko and Milan Češka and Sebastian Junges and Filip Macák},
journal= {arXiv preprint arXiv:2407.12552},
year = {2024}
}
备注
to be published at ATVA 2024