Runtime Monitoring of Perception-Based Autonomous Systems via Embedding Temporal Logic

Runtime monitoring of autonomous systems traditionally relies on mapping continuous sensor observations to discrete logical propositions defined over low-dimensional state variables. This abstraction breaks down in perception-driven settings, where such mappings require additional learned modules that are often computationally expensive, brittle, and semantically misaligned. In this work, we propose Embedding Temporal Logic (ETL), a temporal logic that performs monitoring directly in learned embedding spaces. ETL defines predicates through distances between observed embeddings and target embeddings derived from reference observations. This formulation allows specifications to capture high-level perceptual concepts, such as similarity to visual goals or avoidance of semantic regions, that are difficult or impossible to express using traditional predicates. By composing these predicates with temporal operators, ETL naturally expresses temporally extended and sequential perceptual behaviors. We introduce ETL monitors for evaluating specifications over bounded embedding traces, along with a conformal calibration procedure that provides reliable and safety-oriented predicate evaluation. We evaluate our approach across multiple manipulation environments to show that ETL achieves strong empirical agreement with ground-truth semantics, including accurate monitoring of temporally composed behaviors.

📋 한 줄 요약

**[자율 시스템 / 형식 검증]** 학습된 임베딩 공간에서 직접 시간 논리식을 평가하는 새로운 런타임 모니터링 프레임워크 Embedding Temporal Logic(ETL)을 제안.

🎯 핵심 기여도

전통적 런타임 모니터링이 저차원 상태 변수 위의 명제로의 매핑에 의존하며, 인지 기반 시스템에서는 이 추상화가 무너진다는 문제를 명확화.
임베딩 공간에서 술어를 직접 정의하는 새로운 시간 논리 ETL 제안 — 술어는 관찰 임베딩과 reference 관찰에서 유도된 target 임베딩 사이의 거리로 표현.
시각적 목표 유사성·의미 영역 회피 같은 고수준 지각 개념을 자연스럽게 다루며, 시간 연산자와 결합해 시간적으로 확장된 지각 행동을 표현.
bounded embedding trace에 대한 ETL 모니터와 conformal calibration 절차로 안전 지향 술어 평가의 신뢰성 확보.

💡 핵심 아이디어

인지 기반 자율 시스템에서는 저차원 명제로의 변환이 부서지므로, 형식 명세를 **임베딩 공간 자체**에서 정의하는 편이 자연스럽고 강건하다. 거리 기반 술어가 비전·언어 모델의 고수준 의미를 그대로 활용할 수 있게 해 준다.

🔬 기술적 접근법

**모델/방법론**: 임베딩 공간에서 술어와 시간 연산자를 정의하는 ETL 논리 + bounded trace 평가 모니터.
**핵심 기법**: reference 관찰에서 target 임베딩을 유도해 거리로 술어 정의, 시간 연산자와 합성해 시퀀스 행동 명세, conformal calibration으로 안전 지향 평가 신뢰도 부여.

📊 주요 결과

다수 manipulation 환경에서 ground-truth 의미와 강한 경험적 일치 보고.
시간적으로 합성된 행동 모니터링에서 정확한 평가 확인.
학습된 추가 모듈 없이도 인지 기반 시스템에서 작동.

💭 의의 및 한계

**의의**: 인지 기반 자율 시스템(로봇·자율주행)에서 명세-실행 간 의미 갭을 좁히는 실용적 형식 모니터링 도구. **한계**: 임베딩 공간 자체가 갖는 학습된 편향에 술어 의미가 의존하므로, 임베더 교체 시 명세 일관성 유지 메커니즘은 추가 연구 필요.

🚀 실용적 활용

로봇 매니퓰레이션의 안전 명세("이 시각 목표와 유사", "위험 영역 회피") 런타임 검증.
자율주행 인지 모듈의 비정상 동작 탐지.
시각·언어 명세를 통합한 정책의 사후 검증 인프라.