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.
@cite_21: 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.
@cite_12: 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.
As mentioned, there has been prior work on generating planner independent certificates or proofs for establishing the unsolvability of a given planning problem. Another related direction, has been the effort to generate excuses" for unsolvability of a planning problem @cite_21 @cite_12 . They do not provide an intuitive explanation as to why a problem is unsolvable, but rather identifies initial state values (or some domain model conditions) whose update could make the problem solvable.