无限时域POMDP的验证
人工智能
2020-07-02 v1 计算机科学中的逻辑
摘要
MDP中的验证问题询问：对于任意消解非确定性的策略，坏事发生的概率是否被某个给定阈值所界定。该验证问题常过于悲观，因为其考虑的策略可能依赖于系统完整状态。本文考虑部分可观测MDP的验证问题，其中策略基于系统发出的观测（的历史）做出决策。我们提出一个扩展先前Lovejoy方法实例的抽象-精化框架。实验表明该框架显著提升了方法的可扩展性。
引用
@article{arxiv.2007.00102,
title = {Verification of indefinite-horizon POMDPs},
author = {Alexander Bork and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann},
journal= {arXiv preprint arXiv:2007.00102},
year = {2020}
}
备注
Technical report for ATVA 2020 paper with the same title