Runtime VerificationExpert
Mind the Refinement Gap: When Safe High-Level Robot Plans Produce Unsafe Executions
This preprint audits a trace-completeness assumption in RoboGuard by comparing safety verdicts on surface plans and graph-refined traces under the same LTL specification. In 12 controlled targeted cases the surface plan was accepted while the refined trace was rejected, and in end-to-end SPINE-RoboGuard tests 2 false-safe cases occurred. The work motivates lightweight graph-based trace refinement as a fix for formal safety monitoring of language-enabled planners.