Qualitative analysis of POMDPs with temporal logic specifications for robotics applications
Qualitative analysis of POMDPs with temporal logic specifications for robotics applications
复制标题
针对机器人应用的具有时序逻辑规范的 POMDP 定性分析
DOI：
10.1109/icra.2015.7139019
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Ayush Kanodia
中科院分区：
文献类型：
--
作者：
K. Chatterjee;Martin Chmelík;Raghav Gupta;Ayush Kanodia
我们认为部分可观察马尔可夫决策过程（POMDPs），这是一个标准的框架，机器人应用程序来模拟存在于真实的世界中的不确定性，与时间逻辑规范。线性时间时序逻辑（LTL）中的所有时序逻辑规范都可以表示为奇偶目标。我们研究的定性分析问题POMDPs奇偶目标，要求是否有一个控制器（政策），以确保目标持有概率1（几乎肯定）。虽然定性分析POMDPs与奇偶校验目标是不可判定的，最近的结果表明，当限制到有限的内存政策的问题是EXPTIME完成。虽然这个问题在理论上是棘手的，我们提出了一个实用的方法来解决定性分析问题。我们设计了几种算法来处理指数复杂度，并在机器人应用程序的一些著名POMDP示例上使用了我们的实现。我们的研究结果提供了第一个实用的方法来解决定性分析的机器人运动规划与LTL属性存在的不确定性。
We consider partially observable Markov decision processes (POMDPs), that are a standard framework for robotics applications to model uncertainties present in the real world, with temporal logic specifications. All temporal logic specifications in linear-time temporal logic (LTL) can be expressed as parity objectives. We study the qualitative analysis problem for POMDPs with parity objectives that asks whether there is a controller (policy) to ensure that the objective holds with probability 1 (almost-surely). While the qualitative analysis of POMDPs with parity objectives is undecidable, recent results show that when restricted to finite-memory policies the problem is EXPTIME-complete. While the problem is intractable in theory, we present a practical approach to solve the qualitative analysis problem. We designed several heuristics to deal with the exponential complexity, and have used our implementation on a number of well-known POMDP examples for robotics applications. Our results provide the first practical approach to solve the qualitative analysis of robot motion planning with LTL properties in the presence of uncertainty.