带 Büchi 目标的马尔可夫决策过程定性分析的符号算法
计算机科学与博弈论
2014-11-20 v2
摘要
我们考虑具有以奇偶性目标给出的 ω-正则规约的马尔可夫决策过程 (MDP)。我们研究计算几乎必然获胜状态集的问题，即从这些状态出发能以概率 1 确保目标实现。计算奇偶性目标几乎必然获胜集的算法迭代地使用 Büchi 目标（奇偶性目标的一个特例）几乎必然获胜集的解。我们的贡献如下：首先，我们提出了第一个用于计算带 Büchi 目标的 MDP 几乎必然获胜集的次二次符号算法；与先前已知的需要 O(n^2) 符号步的算法相比，我们的算法需要 O(n √m) 符号步，其中 n 是 MDP 的状态数，m 是边数。在实践中，MDP 具有常数出度，此时我们的符号算法需要 O(n √n) 符号步，而先前已知的算法需要 O(n^2) 符号步。其次，我们提出了一种新算法，即胜负算法，具有以下两个性质：(a) 该算法迭代地计算几乎必然获胜集及其补集的子集，而所有先前算法在终止时才得到几乎必然获胜集；(b) 需要 O(n √K) 符号步，其中 K 是 MDP 的强连通分量 (scc) 的最大边数。胜负算法需要对 scc 进行符号计算。第三，我们改进了符号 scc 计算的算法；先前已知的算法需要线性符号步，而我们的新算法改进了与线性步数相关的常数。在最坏情况下，先前已知的算法需要 5n 符号步，而我们的新算法需要 4n 符号步。
引用
@article{arxiv.1104.3348,
title = {Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with B\"uchi Objectives},
author = {Krishnendu Chatterjee and Monika Henzinger and Manas Joglekar and Nisarg Shah},
journal= {arXiv preprint arXiv:1104.3348},
year = {2014}
}