Planning via model checking with decision-tree controllers

Planning problems can be solved not only by planners, but also by model checkers. While the former yield a plan that requires replanning as soon as any fault occurs, the latter provide a “universal” plan (a. k. a. strategy, policy, or controller) able to make decisions under all circumstances. One of the prohibitive aspects of the latter approach is stemming from this very advantage: since it is defined for all possible states of the system, it is typically so large that it does not fit into small memories of embedded devices. As another consequence of the size, its execution may be slow. In this paper, we provide a solution to this issue by linking the model checkers with decision-tree learners, resulting in decision-tree representations of the synthesized strategies. Not only are they dramatically smaller, but also more explainable and orders-of-magnitude faster to execute than plans with replanning. In addition, we describe a method for model validation and debugging via the model checker and the decision-tree learner in the loop. We illustrate the approach on our case study of a robotic arm for picking items in a real industrial setting.

Authors

• Jonis Kiesbye
• Kush Grover
• Pranav Ashok
• Jan Kretínský

Keywords

• Automation
• Service robots
• Debugging
• Model checking
• Manipulators
• Planning
• Decision Tree
• System State
• Regression Tree
• Robotic Arm
• Probabilistic Model
• Model In Order
• Fault-tolerant
• Lookup Table
• Path Planning
• Active Recovery
• Autonomic Activity
• Markov Decision Process
• Task Planning
• Robot Operating System
• Shared Object
• Temporal Logic
• Problem In Robotics
• Failure Recovery
• Reachable States
• Motion Primitives
• Industrial Case Study
• Influence Diagram
• Fault Scenarios
• Cycle Time
• Binary Tree
• Finite Domain
• Human Operator
• Robot Control