VASS诱导的马尔可夫决策过程(MDP)的定性分析
计算机科学中的逻辑
2016-01-14 v2
摘要
我们考虑由带状态向量加法系统（VASS）的扩展所诱导的无限状态马尔可夫决策过程（MDP）。这些MDP的验证条件由关于给定控制状态集的可达性和Büchi目标描述。我们研究这些目标的某些定性版本的可判定性，即，这些目标是否可被必然、几乎必然或极限必然地达成的可判定性。尽管一般而言此类问题大多不可判定，但对于一些大的子类是可判定的：在这些子类中，要么仅控制器、要么仅随机环境可以改变计数器值（而另一方只能改变控制状态）。
引用
@article{arxiv.1512.08824,
title = {Qualitative Analysis of VASS-Induced MDPs},
author = {Parosh Aziz Abdulla and Radu Ciobanu and Richard Mayr and Arnaud Sangnier and Jeremy Sproston},
journal= {arXiv preprint arXiv:1512.08824},
year = {2016}
}
备注
Extended version (including all proofs) of material presented at FOSSACS 2016