슈퍼마팅게일 인증서로서의 가치 함수 (Value Functions as Supermartingale Certificates)

확률적 시스템 (stochastic systems)을 위한 인증 방법론은 실수 값의 슈퍼마팅게일 인증서 (supermartingale certificates)를 기반으로, 가산 무한 (countably infinite) 및 연속 (continuous) 상태 공간을 모두 포함하는 일반적인 상태 공간에서 $\omega$-정규 속성 ($\omega$-regular properties, 따라서 선형 시제 논리 (linear temporal logic))의 거의 확실한 (almost-sure) 만족 여부를 결정하기 위한 충분한 증명 규칙을 제공합니다. 반대로, $\omega$-정규 작업을 위한 강화학습 (RL) 방법론은 상당한 주목을 받아왔으나, 유한한 상태 및 행동 공간을 제외하고는 학습된 정책 (policy)이 명세 (specification)를 만족한다는 형식적 보장 (formal guarantees)이 일반적으로 부족합니다. 본 연구에서는 새로운 이론적 연결 고리를 구축함으로써 이 두 연구 분야를 잇습니다. 즉, 적절한 보상 (reward) 하에서 $\omega$-정규 속성을 거의 확실하게 만족하는 정책과 관련된 가치 함수 (value function)는 해당 명세에 대한 Streett 슈퍼마팅게일 인증서를 인코딩합니다. 유한 마르코프 결정 과정 (finite Markov decision processes)에서 실험적으로 검증된 우리의 결과는 유한, 가산 무한 및 연속 상태 공간에 대해 유효하며, 이는 RL을 통한 인증서 합성 (certificate synthesis)으로 가는 원칙적인 경로를 제시합니다.