기술 요약: 신호 템포럴 로직(Signal Temporal Logic)을 위한 보상 머신(Reward Machines)

문제 정의

본 논문은 복잡한 실시간 사양(Signal Temporal Logic, STL)으로 정의된 요구사항을 충족해야 하는, 동역학을 알 수 없는 시스템을 위한 제어 정책 합성의 과제를 다룹다. STL은 실수 값 기반의 시간 제약적 동작을 명시하고 정량적인 "강건성(robustness)" 점수를 제공하는 엄격한 언어를 제공하지만, 이 점수를 **강화 학습(RL)**의 보상으로 직접 사용하는 것은 문제가 된다.

핵심적인 어려움은 STL 강건성의 **이력 의존적 의미론(history-dependent semantics)**에 있다. STL 수식의 만족 여부는 종종 전체 실행 궤적에 따라 결정된다(예: "결국 시스템은 5초 동안 특정 영역 내에 머물러야 한다"). 이는 현재 상태에만 보상이 의존한다는 표준 강화 학습 프레임워크의 기본 가정인 **마르코프 성질(Markov property)**을 위반한다. 기존의 해결책들은 방문한 상태의 전체 이력을 상태 공간에 추가함으로써 마르코프 성질을 복구하려고 시도한다. 그러나 이는 특히 중첩된 템포럴 연산자가 있는 긴 호라이즌(long-horizon) 사양의 경우, 다루기 힘든 상태 공간 폭발을 초래한다. 대안적으로, 이전 연구들은 STL의 제한된 파편(fragments)으로 로직을 제한하여 표현력을 희생하기도 했다. 현재로서는 직관적인 이력 증강을 피하면서 전체 STL 사양을 처리할 수 있는 모델 프리(model-free) 접근 방식은 존재하지 않는다.

방법론

저자들은 효율적인 메모리와 마르코프 보상을 제공하기 위해 **보상 머신(Reward Machines, RMs)**을 구축하는 새로운 오토마타 기반 프레임워크를 제안한다. 방법론은 세 가지 주요 단계로 진행된다.

1. 원-클락 교대 타이밍 오토마타(One-Clock Alternating Timed Automata, OCATA)로의 변환

저자들은 관측 사이의 확률적이고 실수 값인 시간 지속 시간을 명시적으로 처리하기 위해 제어 시스템을 **준 마르코프 결정 과정(Semi-Markov Decision Process, SMDP)**으로 모델링한다. 그 후 주어진 STL 사양을 OCATA로 변환한다.

• OCATA 구조: 표준 결정론적 오토마타와 달리, OCATA는 이산적(disjunctive, 존재적/비결정적) 및 결합적(conjunctive, 보편적) 전이를 지원한다.
• 의미론: 이산적 전이는 오토마타가 수용을 향한 경로를 "추측"할 수 있게 하며, 결합적 전이는 모든 조건이 사양을 만족해야 하는 여러 계산 스레드를 생성한다.
• 수용: 오토마타는 뷔치(Büchi) 수용 조건을 사용하며, 이는 수용 위치가 무한히 자주 방문되어야 함을 요구한다.

2. STL-보상 머신(STL-RMs) 구축

OCATA는 메모리 메커니즘이자 보상 생성기 역할을 하는 STL-RM으로 변환된다.

• 메모리 리스트: RM은 특정 "복사본"의 OCATA 상태(위치 및 클락 값)와 그와 관련된 확률 질량(probability mass)을 추적하는 메모리 항목 리스트를 유지한다.
• 분기 처리:
  • 비결정론(Disjunction): RL 에이전트에 의해 선택되는 $\epsilon$-액션에 의해 해결된다.
  • 결합(Conjunction): 결합적 전이가 발생하면, 부모 상태의 확률 질량이 자식 상태들로 분할된다. 만약 전이가 클락 리셋을 포함하면 새로운 메모리 항목이 생성되고, 그렇지 않으면 확률 질량이 기존 항목들 사이에 재분배된다.
• 강건성 통합: 관측 섭동(perturbation)을 처리하기 위해, 저자들은 술어(predicate) 만족에 대한 확률적 해석을 도입한다. 이진 true/false 전이 대신, 관측된 신호 값에 기반하여 술어를 만족할 확률을 계산하는 누적 분포 함수(CDF)를 사용한다. 이는 강건한 만족을 장려하는 "미분 가능한" 전이를 생성한다.
• 보상 생성: RM은 수용 위치에 남아 있는 확률 질량을 기반으로 스칼라 보상을 출력한다. 보상 함수는 기대 누적 수익을 최대화하는 것이 뷔치 조건을 만족할 확률을 최대화하는 것과 일치하도록 설계되었다.

3. 마르코프 RL을 위한 곱 생성(Product Construction)

SMDP와 STL-RM은 **곱 MDP(Product MDP)**로 결합된다.

• 상태 증강: 곱 MDP의 상태 공간은 환경 상태, 시간 지속 시간, 그리고 RM의 메모리 리스트의 데카르트 곱이다.
• 마르코프 성질: 메모리 리스트를 상태에 포함함으로써, 보상 함수는 마르코프적(현재의 증강된 상태에만 의존)이 되어 표준 오프더쉘프(off-the-shelf) RL 알고리즘(예: PPO)을 사용할 수 있게 된다.
• 이론적 보장: 저자들은 만약 정책이 곱 MDP에서 최대 기대 수익 1을 달성하면, 확률 1로 원래의 STL 사양을 만족한다는 것을 증명한다.

주요 기여

1. 새로운 오토마타 기반 프레임워크: 본 논문은 STL 사양을 OCATA로 컴파일하고 이후 STL-RM으로 컴파일함으로써, 전체 STL 사양으로부터 컨트롤러를 학습하는 방법을 소개한다. 이 접근 방식은 확률적 시스템을 SMDP로 모델링하고 이벤트 기반 STL 의미론을 채택한다.
2. 효율적인 메모리 및 마르코프 보상: 제안된 STL-RM은 마르코프 보상을 유도하는 압축된 메모리 메커니즘(오토마타 위치 및 클락 값 추적)을 제공한다. 이는 전체 이력을 증강할 때 발생하는 다루기 힘든 상태 확장을 피하면서도 표준 RL 알고리즘과의 호환성을 유지한다.
3. 강건성을 고려한 전이: 프레임워크는 이진 만족에만 의존하는 대신, 미분 가능한 보상 개념에서 유도된 확률적 전이를 사용하여 관측 섭동에 대한 강건성을 포함한다.
4. 이론적 및 경험적 검증: 저자들은 자신들의 프레임워크에서 누적 보상을 최대화하는 것이 사양 만족을 확률 1로 보장함을 공식화한다. 경험적으로, 다양한 제어 환경에서 이들의 방식이 이력 기반 베이스라인(관측 스태킹 및 순환 신경망)에 비해 더 빠르게 정책을 학습하고 더 높은 만족도와 강건성 점수를 달성함을 입증한다.

실험 결과

저자들은 다섯 가지 벤치마크 환경(CartPole, Reacher, Pusher, Fetch, Adroit)에서 두 가지 유형의 STL 사양을 사용하여 STL-RM을 평가했다.

• 부분 사양(Partial Specification): 무제한 템포럴 연산자(순서 지정 및 안전성).
• 전체 사양(Full Specification): 경계 시간 안정성 요구사항(특정 시간 창 내에 시스템이 중앙 영역으로 돌아와야 함)을 포함함.

결과:

• 성능: STL-RM(및 그 이산 버전)은 특히 전체 사양에서 만족도 비율과 강건성 점수 측면에서 베이스라인(다양한 윈도우 크기를 가진 스태킹 및 LSTM 기반 순환 정책)을 일관되게 능가했다.
• 확장성: 베이스라인은 (원시 이력으로부터 템포럴 컨텍스트를 학습하는 어려움 때문에) 전체 사양의 경계 시간 요구사항을 수행하는 데 크게 어려움을 겪은 반면, STL-RM은 최적에 가까운 정책으로 수렴했다.
• 강건성: 연속적이고 강건성을 고려한 STL-RM 변형은 일반적으로 이산 변형보다 높은 강건성 점수를 달절했는데, 이는 확률적 전이가 더 큰 안전 마진을 가지고 사양을 만족하는 정책을 장려함을 시사한다.

의의 및 주장

본 논문은 표준 RL이 과도한 계산 비용 없이 전체 STL 사양의 이력 의존적 특성을 처리할 수 없다는 모델 프리 제어 합성의 핵심 병목 현상을 해결한다고 주장한다.

• 표현력: 특정 STL 파편으로 제한되는 이전 연구들과 달리, 이 접근 방식은 임의로 중첩된 템포럴 연산자를 가진 전체 STL을 지원한다.
• 효율성: 원시 이력 스태킹 대신 오토마타 기반 메모리를 사용함으로써, 이 방법은 "상태 폭발" 문제를 피하고 긴 호라이즌 작업을 수행할 수 있게 한다.
• 실용성: 프레임워크는 기존 RL 도구(예: PPO)와 호환되며 시스템 모델을 필요로 하지 않는다.
• 한계점: 저자들은 메모리 용량이 유한하다는 점을 겸허히 인정한다. 많은 동시 템포럴 의무가 있는 시나리오에서는 메모리 리스트가 커질 수 있으며, 향후 연구에서 프루닝(pruning)이나 더 압축된 표현(예: 구간 기반)이 필요할 수 있다.

본 논문은 오토마타 기반 보상 설계가 복잡한 모델 프리 환경에서 표현력이 풍부한 템포럴 로직 사양으로부터 컨트롤러를 합성하는 데 있어 유망한 방향임을 결론짓는다.