Value Functions for Temporal Logic: Optimal Policies and Safety Filters

기술적 요약: 시간 논리를 위한 가치 함수: 최적 정책 및 안전 필터

문제 제기
기본적인 도달 (reach), 회피 (avoid), 도달 - 회피 (reach-avoid) 문제에 대한 벨만 방정식은 잘 정립되어 있지만, 가치 최적성과 정책 최적성 간의 관계는 할인되지 않은 무한 시간 범위 설정에서, 특히 복잡한 시간 논리 (TL) 명세에 대해서는 미묘해집니다. Until 명세와 동등한 도달 - 회피 문제에서 Q-함수를 탐욕적으로 최대화하는 것이 가치 함수 자체는 최적임에도 불구하고 작업 완료를 무한히 지연시키는 정책을 생성하는 치명적인 병리 현상이 발생합니다. 이는 무한 궤적에 대한 최적의 동작 시퀀스가 근본적으로 비마르코프적 (non-Markovian) 이기 때문입니다. 최적 입력은 남은 무한 시간 범위 명세를 충족시키기 위해 분해 그래프의 구성 가치 함수 중 하나를 최대화하는 것으로부터 현재 가치를 최대화하는 것으로 "전환"해야 할 수 있습니다. 이중 목적 문제의 상태 확장 (state-augmentation) 과 같은 기존 방법들은 중첩된 Until, Globally, 그리고 Globally-Until 명세를 포함하는 복잡한 수식에 대해 일반화하는 데 어려움을 겪습니다. 또한 단순한 회피 또는 도달 - 회피 작업을 넘어 복잡한 TL 명세의 만족을 보장하는 안전 필터의 필요성이 있습니다.

방법론
저자들은 문제의 비마르코프적 특성을 처리하기 위해 상태 히스토리에 대한 가치 함수와 Q-함수를 일반화하는 프레임워크를 제안합니다. 이 방법론은 TL 에 대한 가치 함수를 구성 가치 함수들의 그래프로 대수적으로 분해하는 데 의존합니다.

1. 비마르코프적 가치 함수: 이 논문은 최적 가치 함수 $V^*$와 Q-함수 $Q$를 현재 상태뿐만 아니라 상태 히스토리 $x_{0:t}$에 대해 정의합니다. 이를 통해 정책이 시간적 제약을 충족하는 데 필요한 히스토리를 고려할 수 있게 됩니다.
2. 시간 확장 시스템 및 증인 시간: Until ($U$) 명세에서의 지연 문제를 해결하기 위해 저자들은 타이머가 포함된 시간 확장 시스템을 도입합니다. 그들은 궤적이 최적의 강건성 점수를 달성하는 가장 초기 시간을 의미하는 "최적 증인 시간" $\sigma^*$을 정의합니다. 이를 통해 증인 시간 내에서 Q-함수를 최대화하는 유한 시간 범위 탐욕 전략에서 나머지 부분 수식을 충족하는 접미사 정책으로 전환하는 정책을 구성할 수 있습니다.
3. 구성적 정책 구성: 이 논문은 특정 TL 수식 조각 (정의 3) 에 대한 최적 정책을 구성합니다. 여기에는 다음이 포함됩니다:
   • 명제 수식.
   • Until ($p U \phi$), Next ($X\phi$), 그리고 Globally ($Gp$) 연산자.
   • Büchi 수용 기준을 인코딩하는 Globally-Until ($G(\bigvee p_i U r_i)$).
   • 논리합 및 명제 논리곱.
     이 구성은 부분 수식에 대한 최적 정책의 존재 (가정 2) 를 가정하고 이를 재귀적으로 결합합니다. Globally-Until의 경우, 정책은 필요한 상태 집합으로의 무한 방문을 보장하기 위해 각 Until 구성 요소를 순차적으로 반복적으로 방문합니다.
4. 안전 필터링: 저자들은 Q-함수가 안전 필터로 작용할 수 있음을 보여줍니다. 그들은 명식이 음이 아닌 강건성으로 충족될 수 없는 실패 집합을 정의합니다. 최소 제한적 개입 방식을 제안합니다: 명목 정책의 동작이 음이 아닌 Q-값 (미래 충족 가능성 표시) 을 생성하면 이를 허용하고, 그렇지 않으면 시스템이 Q-함수를 최대화하는 동작으로 전환합니다. 특정 가정 (예: 무제한 Until 연산자의 부재) 하에서 이 필터는 명식 만족을 보장합니다.

주요 기여

1. 가치 함수의 일반화: 이 논문은 최적 가치 함수와 Q-함수를 상태 히스토리로 일반화 (정의 1) 하고 히스토리에서의 최적성을 정의 (정의 2) 하여 무한 시간 범위 TL 문제의 비마르코프적 특성을 다룹니다.
2. 구성적 최적 정책: 광범위한 클래스의 TL 수식 (정의 3) 에 대해 저자들은 관련 강건성 지표에 대한 구성적 최적 정책을 구성합니다 (정리 1–8). 여기에는 Until 및 Globally-Until 명세에서의 지연 병리 현상을 처리하는 것이 포함됩니다.
3. 최소 제한적 안전 필터: 이 연구는 (잠재적으로 비최적인) 히스토리에 대한 Q-함수가 명목 정책에 대한 최소 제한적 안전 필터를 생성함을 보여줍니다 (정리 9, 10). 이 필터는 수식이 특정 구조적 제약을 충족하는 한, 명목 정책의 이전 경로를 존중하면서 명식 만족을 보장합니다.

결과 및 시연
이 논문은 이론적 증명과 두 가지 하드웨어/소프트웨어 시연을 통해 제안된 프레임워크를 검증합니다:

• 2 에이전트 그리드 월드: 저자들은 시간 제한 도달, 안전, 그리고 활성성 제약을 포함하는 복잡한 명세를 가진 4 차원 결합 상태 - 동작 문제를 해결합니다. 유도된 최적 정책 ($\pi_{spec}$) 이 시스템을 성공적으로 안내하여 명식을 만족함을 시연합니다. 또한 "커피" 및 "차" 명목 정책 (각각 단독으로는 결합 명식을 충족하지 못함) 에 대한 필터로 사용될 때, 이 필터는 결합 시스템이 복잡한 작업을 충족하도록 보장하는 반면, 표준 "안전 전용" 필터는 교착 상태와 실패로 이어집니다.
• 단일 에이전트 드론: Crazyflie 드론을 사용하여 저자들은 장애물이 있는 항법 작업에서 정책을 시연합니다. 제안된 TL 필터는 드론을 특정 구역 순회 및 벽 회피와 같은 복잡한 시간 제약을 충족시키면서 작업 현장으로 성공적으로 안내합니다. 반면, 필터링되지 않은 명목 정책이나 안전 제약만 기반한 필터는 드론이 갇히거나 추락하는 결과를 초래합니다.

의의
이 논문은 최근 분해 결과를 확장하여 광범위한 클래스의 TL 수식에 대한 가치 최적 정책을 생성하는 실용적인 접근법을 제공한다고 주장합니다. 이의 주요 의의는 무한 시간 범위 작업에서 탐욕적 Q-최대화가 실패하는 병리 현상을 해결하고, 단순한 안전이 아닌 복잡한 작업 만족을 보장하는 안전 필터를 합성하는 메커니즘을 제공하는 데 있습니다. 중첩된 Until 및 Globally-Until 명세를 포함하도록 해결 가능한 수식의 범위를 확장함으로써, 이 연구는 복잡한 안전-중요 시간 작업에 대한 해밀턴 - 야코비 도달성 및 강화 학습 간의 간극을 메웁니다.