SemML 2.0: 선형 시간 논리(LTL)를 위한 제어기 합성

SemML 2.0: Synthesizing Controllers for LTL

선형 시간 논리(LTL)로 주어진 명세로부터 반응형 시스템을 합성하는 문제는 안전이 중요한 시스템 설계에 널리 활용되는 고전적인 문제입니다. 이러한 시스템은 일반적으로 Mealy 머신 또는 AIGER 회로를 사용하여 표현됩니다. 본 논문에서는 기존 최고 성능 도구들을 능가하는 SemML의 두 번째 버전을 소개합니다. SemML은 고전적인 자동자 이론 기반 접근 방식을 구현할 뿐만 아니라, 효율적인 솔루션 탐색을 위해 부분 탐색 및 머신 러닝 기반 지침을 활용하며, 또한 솔루션의 작은 표현을 추출하기 위한 다양한 휴리스틱과 기존 알고리즘의 개선 사항을 적용했습니다. 저희 도구를 SYNTCOMP 합성 대회 데이터 세트를 사용하여 기존 최고 성능 도구(특히 Strix, LtlSynt 및 SemML의 이전 버전)와 비교 평가했습니다. 그 결과, 저희 도구는 다른 도구보다 훨씬 더 많은 문제를 해결하고, 훨씬 빠르게 해결하며, 동시에 최고 수준의 솔루션 품질을 유지하는 것을 확인했습니다.

Synthesizing a reactive system from specifications given in linear temporal logic (LTL) is a classical problem, finding its applications in safety-critical systems design. These systems are typically represented using either Mealy machines or AIGER circuits. We present the second version of SemML, which outperforms all state-of-the-art tools for finding either solution. Aside from implementing the classical automata-theoretic approach, our tool utilizes partial exploration and machine-learning guidance for obtaining solutions efficiently, and numerous heuristics and improvements of classic algorithms for extracting small representations of these solutions. We evaluate our tool against the existing state-of-the-art tools (in particular Strix, LtlSynt, and the previous version of SemML) on the dataset of the synthesis competition SYNTCOMP. We show that we solve significantly more instances and do so much faster than other tools, while maintaining state-of-the-art solution quality.