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

요약

컴포넌트 기반 합성(CBS) 과정에서 정밀한 제약 조건으로 인해 발생하는 탐색 효율성 저하 문제를 해결하기 위한 새로운 방법론을 제안합니다. 논리적 유사성을 추론하기 위해 정제 타입 명세를 활용하는 '액체 트리 오토마타(Liquid Tree Automata, LTA)'를 도입하여 중복 탐색을 방지합니다.

핵심 포인트

• 정밀한 질의와 제약 조건이 늘어날수록 유효한 경로를 찾기 어려워지는 CBS의 한계를 지적함
• 정제 타입 명세와 서브타이핑 제약 조건을 활용하는 새로운 트리 오토마타 변형인 LTA를 제안함
• LTA는 의미론적으로 유사한 상태를 식별하고 병합함으로써 탐색 효율성을 극대화함
• 구현 도구인 Hegel은 기존 최첨단 도구들이 해결하지 못한 복잡한 질의에 대한 솔루션을 합성할 수 있음을 입증함