Runtime Verification전문가
RoboGuard의 정제 격차, 안전한 상위 계획이 불안전한 실행을 만든다
이 프리프린트는 로봇 계획의 상위 행동 추적만 검증하는 RoboGuard가 그래프 상 중간 경유지와 암묵적 이동을 반영한 실행 추적에서는 같은 LTL 규칙을 위반할 수 있음을 보였다. 통제 평가 28개 사례에서 표적 추상화 12개 전부가 표면 계획은 안전, 정제 추적은 불안전으로 갈렸고, SPINE과 RoboGuard를 연동한 14개 사례에서도 2건의 거짓 안전이 확인됐다. 그래프 기반 추적 정제를 감시 전에 적용하면 판정 시간이 0.54ms에서 0.69ms로만 늘며 이 격차를 드러낼 수 있어, 계획기와 실행기와 감시기 사이의 명시적 추적 계약이 필요하다.