Counterexamples for Robotic Planning Explained in Structured Language

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.

Authors

• Lu Feng 0001
• Mahsa Ghasemi
• Kai-Wei Chang 0001
• Ufuk Topcu

Keywords

• Robots
• Natural languages
• Planning
• Computational modeling
• Charging stations
• Model checking
• Markov processes
• Language Structure
• Planning Of Robots
• Natural Language
• Mixed-integer Programming
• Markov Decision Process
• Mixed Integer Linear Programming
• Robot Behavior
• Markov Decision Process Model
• Magnetic Field
• Minimalist
• Target State
• Probability Threshold
• North Of Area
• Robot Control
• Real Variables
• Map Scale
• Complete Explanation
• Number Of Sentences
• Safety Properties
• Number Of Binary Variables
• Mixed Integer Linear Programming Formulation
• Set Of Propositions
• Areas Of Delivery