# Counterexamples for Robotic Planning Explained in Structured Language

## TL;DR

This paper introduces a method to generate human-understandable counterexamples for robotic planning models using structured natural language, improving interpretability of verification artifacts.

## Contribution

It proposes a mixed-integer linear programming approach to produce minimal, sound, and complete explainable counterexamples in natural language for MDP-based robotic plans.

## Key findings

- Effective generation of natural language counterexamples demonstrated in warehouse robot case study.
- Improved interpretability of verification results for robotic mission plans.
- Method produces concise, comprehensive explanations of requirement violations.

## Abstract

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.