不確実環境における確率的満足保証付きLTL制御
LTL Control in Uncertain Environments with Probabilistic Satisfaction Guarantees
環境の不確実性と雑音のあるセンサ・アクチュエータを考慮し、LTL式で与えられたタスクを達成する確率を最大化するロボット制御戦略を、MDP上の確率モデル検査を用いて生成する手法を提案した。
著者: Xu Chu Ding, Stephen L. Smith, Calin Belta, Daniela Rus
分類: math.OC, cs.RO, cs.SY, eess.SY
原文アブストラクト
We present a method to generate a robot control strategy that maximizes the probability to accomplish a task. The task is given as a Linear Temporal Logic (LTL) formula over a set of properties that can be satisfied at the regions of a partitioned environment. We assume that the probabilities with which the properties are satisfied at the regions are known, and the robot can determine the truth value of a proposition only at the current region. Motivated by several results on partitioned-based abstractions, we assume that the motion is performed on a graph. To account for noisy sensors and actuators, we assume that a control action enables several transitions with known probabilities. We show that this problem can be reduced to the problem of generating a control policy for a Markov Decision Process (MDP) such that the probability of satisfying an LTL formula over its states is maximized. We provide a complete solution for the latter problem that builds on existing results from probabilistic model checking. We include an illustrative case study.
