다중 속성 합성

Multi-Property Synthesis

우리는 모든 속성을 만족하는 것이 불가능할 수 있는 상황에서의 다중 속성 LTLf 합성을 연구한다. 속성의 부분집합을 일일이 나열하는 대신, 단일 고정점(fixed-point) 계산을 통해 곱 게임(product-game) 상태와 그 상태에서 실현 가능한 목표 집합 간의 관계를 산출하고, 실현 가능한 최대 집합을 달성하는 전략을 합성한다. 우리는 불린(Boolean) 목표 변수를 도입하고 단조성(monotonicity)을 활용하여 지수적으로 많은 목표 조합을 간결하게 표현하는 완전 기호(fully symbolic) 알고리즘을 개발한다. 우리의 접근 방식은 열거 기반의 베이스라인보다 월등히 뛰어난 성능을 보이며, 최대 100배의 속도 향상을 달성한다.

We study LTLf synthesis with multiple properties, where satisfying all properties may be impossible. Instead of enumerating subsets of properties, we compute in one fixed-point computation the relation between product-game states and the goal sets that are realizable from them, and we synthesize strategies achieving maximal realizable sets. We develop a fully symbolic algorithm that introduces Boolean goal variables and exploits monotonicity to represent exponentially many goal combinations compactly. Our approach substantially outperforms enumeration-based baselines, with speedups of up to two orders of magnitude.