ω-正则目标部分可观测马氏决策过程的可判定性
What is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives
摘要：
我们考虑部分可观测马尔可夫决策过程（POMDPs）的ω-正则条件指定为奇偶性目标。ω-正则语言类将正则语言扩展到无限串，并提供了一种健壮的规约语言来表达验证中使用的所有属性，奇偶目标是表示ω-正则条件的规范形式。给定一个POMDP和一个奇偶性目标的定性分析问题是问是否有一个策略来确保目标满足概率1（分别为1和1）。正概率）。虽然定性分析问题是不可判定的，即使是非常特殊的情况下的奇偶性目标，我们建立了可判定性（最佳复杂度）的POMDP与所有奇偶性目标下的有限记忆策略的定性分析问题。我们建立了最佳（指数）的记忆边界和EXPTIME-完全性的定性分析问题的POMDPs奇偶目标的有限记忆策略下。
英文摘要：
We consider partially observable Markov decision processes (POMDPs) with ω-regular conditions specified as parity objectives. The class of ω-regular languages extends regular languages to infinite strings and provides a robust specification language to express all properties used in verification, and parity objectives are canonical forms to express ω-regular conditions. The qualitative analysis problem given a POMDP and a parity objective asks whether there is a strategy to ensure that the objective is satis- fied with probability 1 (resp. positive probability). While the qualitative analysis problems are known to be undecidable even for very special cases of parity objectives, we establish decidability (with optimal complexity) of the qualitative analysis problems for POMDPs with all parity objectives under finite- memory strategies. We establish optimal (exponential) memory bounds and EXPTIME-completeness of the qualitative analysis problems under finite-memory strategies for POMDPs with parity objectives.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
