Explainable planning is widely accepted as a prerequisite for autonomous agents to successfully work with humans. While there has been a lot of research on generating explanations of solutions to planning problems, explaining the absence of solutions remains an open and under-studied problem, even though such situations can be the hardest to understand or debug. In this paper, we show that hierarchical abstractions can be used to efficiently generate reasons for unsolvability of planning problems. In contrast to related work on computing certificates of unsolvability, we show that these methods can generate compact, human-understandable reasons for unsolvability. Empirical analysis and user studies show the validity of our methods as well as their computational efficacy on a number of benchmark planning domains.
Another closely related direction has been the work done on explaining unsynthesizability of hybrid controllers for a given set of high-level task specifications @cite_4 . The work tries to identify the subformulas of the given specification that lead to the unsynthesizability. This particular approach is specific to the planning framework detailed in @cite_17 and the objective of the work parallels the goals of work like @cite_21 @cite_12 .
@cite_21 @cite_4 @cite_12 @cite_17
2161103575 2027175684 2397809688 2004796166
When using a planner-based agent architecture, many things can go wrong. First and foremost, an agent might fail to execute one of the planned actions for some reasons. Even more annoying, however, is a situation where the agent is incompetent, i.e., unable to come up with a plan. This might be due to the fact that there are principal reasons that prohibit a successful plan or simply because the task's description is incomplete or incorrect. In either case, an explanation for such a failure would be very helpful. We will address this problem and provide a formalization of coming up with excuses for not being able to find a plan. Based on that, we will present an algorithm that is able to find excuses and demonstrate that such excuses can be found in practical settings in reasonable time. High-level robot control has recently seen the application of formal methods to the automatic synthesis of correct-by-construction controllers from user-defined specifications. When a specification fails to yield a corresponding controller, existing techniques provide feedback on portions of the specification that cause the failure, but at a coarse granularity. This work provides techniques for extracting minimal explanations of such failures. The approach is shown to provide refinement of the feedback on several example specifications. When a planning task cannot be solved then it can often be made solvable by modifying it a bit: one may change either the set of actions, or the initial state, or the goal description. We show that modification of actions can be reduced to initial state modification. We then apply Katsuno and Mendelzon's distinction between update and revision and show that the modification of the initial state is an update and the modification of the goal description is a revision. We consider variants of Forbus's update and Dalal's revision operation and argue that existing belief change operations do not apply as they stand because their inputs are boolean formulas, while plan task modification involves counterfactual statements. We show that they can be captured in Dynamic Logic of Propositional Assignments DL-PA. The Linear Temporal Logic MissiOn Planning (LTLMoP) toolkit is a software package designed to assist in the rapid development, implementation, and testing of high-level robot controllers. In this toolkit, structured English and Linear Temporal Logic are used to write high-level reactive task specifications, which are then automatically transformed into correct robot controllers that can be used to drive either a simulated or a real robot. LTLMoP's modular design makes it ideal for research in areas such as controller synthesis, semantic parsing, motion planning, and human-robot interaction.