액체 트리 오토마타 (Liquid Tree Automata)

컴포넌트 기반 합성 (Component-based synthesis, CBS)은 논리적 질의 (logical queries)를 충족하기 위해 라이브러리 컴포넌트로부터 루프가 없는 프로그램을 생성합니다. 표현력이 풍부한 명세 (specifications)와 정밀한 질의는 솔루션 공간을 단순화하지만, 전통적인 CBS 절차에서는 실행 가능한 경로를 찾는 것을 훨씬 더 어렵게 만듭니다. 제약 조건이 더 정확해질수록, 탐색은 유효한 경로가 점점 더 희소해지는 공간을 탐색해야 합니다. 우리는 탐색 경로 간의 extit{논리적 유사성 (logical similarities)}에 대해 추론함으로써 이 문제를 해결합니다. 우리는 기본 타입을 논리적 한정자 (logical qualifiers)로 보강하여 값 공간을 정밀하게 제한하는 정제 타입 명세 (refinement-type specifications)가 갖춰진 라이브러리 메서드를 고려합니다. 이 공간을 효율적으로 탐색하기 위해, 우리는 정제 타이핑 규칙 (refinement typing rules)에 의해 구축되는 새로운 트리 오토마타 (tree automata) 변형인 액체 트리 오토마타 (Liquid Tree Automata, LTA)를 도입합니다. LTA는 서브타이핑 제약 조건 (subtyping constraints)을 활용하여 탐색 중에 의미론적으로 유사한 상태를 식별하고 적극적으로 병합합니다. 이러한 병합은 동일한 경로에 대한 중복 탐색을 방지하여 합성 효율성을 크게 향상시킵니다. 우리는 이 접근 방식을 Hegel이라는 도구로 구현했습니다. 우리의 평가 결과, Hegel은 기존의 최첨단 (state-of-the-art) 도구들이 도달할 수 없는 복잡한 질의에 대한 솔루션을 합성함을 입증했습니다.