Specification-grounded explanation synthesis for spatio-temporal logic monitoring in robotics

Abstract

Runtime monitoring enables robots to verify compliance with formally specified safety and task requirements during execution. However, monitoring frameworks typically provide verdicts, robustness values, or counterexamples that are difficult for operators to interpret. Existing explanation approaches often rely on manually curated templates with limited coverage or leverage large language models that lack guarantees of semantic correctness. This paper presents a specification-grounded explanation framework for spatio-temporal logic monitoring in robotics. The proposed approach synthesizes explanations directly from specification semantics using a compositional grammar. By leveraging monitor information, the framework identifies the spatial relations, temporal obligations, and objects responsible for warnings and violations, and generates concise textual explanations and geometric evidence. We evaluate the approach on a collaborative robotic manipulation task and demonstrate real-time online performance. Experiments on 120 manually annotated test cases show that the proposed method achieves higher completeness and soundness than pattern-based and LLM-based baselines.