What is decidable about partially observable Markov decision processes with ω-regular objectives
What is decidable about partially observable Markov decision processes with ω-regular objectives
复制标题
DOI：
10.1016/j.jcss.2016.02.009
复制
发表时间：
2016-08-01
影响因子：
1.1
通讯作者：
Tracol, Mathieu
中科院分区：
文献类型：
--
作者：
Chatterjee, Krishnendu;Chmelik, Martin;Tracol, Mathieu
我们考虑部分可观测马尔可夫决策过程（POMDPs）的ω-定期条件指定为奇偶校验目标。Omega正则语言类提供了一种鲁棒的规范语言来表达验证中的属性，奇偶目标是表达它们的规范形式。给定POMDP和奇偶性目标的定性分析问题询问是否存在策略以确保目标以概率1（分别为1）满足。正概率）。虽然定性分析问题是不可判定的，即使是特殊情况下的奇偶校验目标，我们建立可判定性（最佳复杂性）POMDPs与所有奇偶校验目标下有限的内存策略。我们建立了最佳（指数）的记忆边界和EXPTIME-完全性的定性分析问题的POMDPs奇偶目标的有限记忆策略下。我们还提出了一个实用的方法，我们设计的算法来处理指数复杂度，并已应用我们的实施上的POMDP的例子。(C)2016 Elsevier Inc. All rights reserved.
We consider partially observable Markov decision processes (POMDPs) with omega-regular conditions specified as parity objectives. The class of omega-regular languages provides a robust specification language to express properties in verification, and parity objectives are canonical forms to express them. The qualitative analysis problem given a POMDP and a parity objective asks whether there is a strategy to ensure that the objective is satisfied with probability 1 (resp. positive probability). While the qualitative analysis problems are undecidable even for special cases of parity objectives, we establish decidability (with optimal complexity) 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. We also present a practical approach, where we design heuristics to deal with the exponential complexity, and have applied our implementation on a number of POMDP examples. (C) 2016 Elsevier Inc. All rights reserved.