有界参数马尔可夫决策过程中 ω-正则性质的满足概率界
计算机科学中的逻辑
2022-07-28 v1 系统与控制
系统与控制
摘要
我们考虑在有界参数马尔可夫决策过程（BMDP）中计算满足一个 ω-正则性质的最小和最大概率的问题。BMDP 由马尔可夫决策过程（MDP）衍生而来，其允许以区间形式对转移概率存在不确定性，即实际概率未知。ω-正则语言构成了一大类性质，可表达为例如 Rabin 或奇偶性自动机，并涵盖诸如线性时序逻辑等丰富规约。在 BMDP 中，满足该性质的概率取决于未知的转移概率以及策略。本文中，我们计算这些极值。这解决了 Dutreix 与 Coogan 在 CDC 2018 中具体指出的问题，并将其关于无对抗者的区间马尔可夫链的结果进行了推广。主要思想是将他们的工作重新解释为区间 MDP 的分析，并相应地将 BMDP 问题视为 ω-正则随机博弈的分析，其中给出了一种解法。该方法可平滑地进一步推广到有界参数随机博弈。
引用
@article{arxiv.2207.13660,
title = {Satisfiability Bounds for $\omega$-Regular Properties in Bounded-Parameter Markov Decision Processes},
author = {Jan Křetínský and Tobias Meggendorfer and Maximilian Weininger},
journal= {arXiv preprint arXiv:2207.13660},
year = {2022}
}