構造化言語で説明するロボット計画の反例生成
Counterexamples for Robotic Planning Explained in Structured Language
ロボットのミッション計画のMDPモデルにおいて、要件違反に至る行動を構造化自然言語で説明する「説明可能な反例」を定義し、混合整数線形計画法で最小かつ健全・完全な反例を生成する手法を提案した。倉庫ロボットの計画事例で有用性を示した。
著者: Lu Feng, Mahsa Ghasemi, Kai-Wei Chang, Ufuk Topcu
分類: cs.RO, cs.CL, cs.FL
原文アブストラクト
Automated techniques such as model checking have been used to verify models of robotic mission plans based on Markov decision processes (MDPs) and generate counterexamples that may help diagnose requirement violations. However, such artifacts may be too complex for humans to understand, because existing representations of counterexamples typically include a large number of paths or a complex automaton. To help improve the interpretability of counterexamples, we define a notion of explainable counterexample, which includes a set of structured natural language sentences to describe the robotic behavior that lead to a requirement violation in an MDP model of robotic mission plan. We propose an approach based on mixed-integer linear programming for generating explainable counterexamples that are minimal, sound and complete. We demonstrate the usefulness of the proposed approach via a case study of warehouse robots planning.
