기술 요약: Kofola 1.0 – $\omega$-정규 언어 보충 및 포함성 검사를 위한 모듈식 접근법

문제 제기

뷰키 오토마타 (BAs) 에 대한 언어 포함성 검사는 모델 체킹, 모니터링, 그리고 정리 증명에서 결정적인 응용을 가진 오토마타 이론적 검증의 근본적인 문제입니다. 이 문제는 PSpace-완전 (PSpace-complete) 이며, 시스템 명세가 크기와 복잡성 측면에서 성장함에 따라 계산적으로 여전히 요구도가 높습니다. $L_1 \subseteq L_2$인지 결정하는 문제는 $L_2$의 여집합인 $\overline{L_2}$에 대해 $L_1 \cap \overline{L_2}$의 공집합성을 검사하는 문제로 환원됩니다. 이 환원은 두 가지 주요 과제를 제시합니다:

1. 컴팩트한 보충 (Compact Complementation): 상태 공간 폭발을 유발하지 않고 효율적으로 여집합 오토마타 $\overline{L_2}$를 구성하는 것.
2. 효율적인 탐색: 종종 거대한 $L_1 \cap \overline{L_2}$의 곱 오토마타를 탐색하는 것.

기존 도구들은 주로 30 년 이상 거슬러 올라가는 고전적인 램지 기반 또는 결정화 기반 보충 구성에 크게 의존합니다. 최근 보충 분야에서 진전이 있었으나, 이들은 실용적인 포함성 검사기에 완전히 통합되지 않았습니다.

방법론

본 논문은 최첨단 모듈식 보충 프레임워크를 구현한 C++ 로 작성된 효율적인 도구인 Kofola를 제시합니다. 이 방법론은 입력 오토마타를 강연결 요소 (SCCs) 로 분해하고, 각 구성 요소의 구조적 속성에 기반하여 맞춤형 보충 알고리즘을 적용하는 데 기반을 둡니다.

1. 구조적 분해 및 구성 요소 분류

Kofola 는 보충될 오토마타 ($A_2$) 에 대한 세밀한 구조적 분석을 수행합니다. 이는 최대 SCC 를 네 가지 뚜렷한 범주로 분류합니다:

• 비수용 구성 요소 (Non-accepting components): 전통적인 부분집합 구성을 통해 처리됩니다.
• 본질적으로 약한 수용 구성 요소 (IWACs): 모든 사이클이 수용하는 구성 요소.
• 결정적 수용 구성 요소 (DACs): 결정적 전이만 있는 구성 요소.
• 초기 거의 결정적 수용 구성 요소 (IADACs): 본 논문에서 새로 식별된 구성 요소 유형입니다. 이들은 초기 상태에서 결정적 SCC 를 통해 도달 가능하며, SCC 간의 비순환 경로에서만 비결정성이 허용되는 결정적 SCC 입니다.
• 비결정적 수용 구성 요소 (NACs): 나머지 수용 SCC 들입니다.

2. 모듈식 보충 프레임워크

각 구성 요소 유형에 대해 Kofola 는 전용 부분 보충 알고리즘을 적용합니다:

• IWACs: $Inf(1)$ 수용 조건을 생성하는 고전적인 미야노 - 하야시 (Miyano-Hayashi) 구성을 사용합니다.
• DACs: $Inf(2)$ 수용 조건을 생성하는 NCSB 알고리즘의 변형을 사용합니다.
• NACs: 작업에 따라 두 가지 접근 방식을 지원합니다:
  • 보충: 더 작은 오토마타를 생성하기 위해 결정화 기반 접근법 (Safra-Piterman 변형) 을 사용합니다.
  • 포함성 검사: 온더플라이 (on-the-fly) 곱 공집합성 테스트에 더 적합한 슬라이스 기반 접근법을 사용합니다.
• IADACs: 논문은 이러한 구성 요소에 대한 새로운 부분 알고리즘을 소개합니다. 이는 부분집합 구성을 사용하여 IADAC 를 결정화하며, 추적된 실행이 수용 전이를 볼 때마다 거부 마크 ($Fin(0)$) 를 방출합니다. 정합성은 IADAC 내의 실행이 제한된 비결정성으로 인해 유한하게 제한된다는 사실에 의존합니다.

최상위 알고리즘은 이러한 부분 구성을 동기화합니다. 결과적으로 생성된 여집합 오토마타는 $Fin(0) \land Inf(1) \land \dots \land Inf(k-1)$ 형태의 단일 수용 조건을 갖는 단순 일반화 라빈 오토마타 (SGRA) 입니다.

3. 온더플라이 공집합성 검사

포함성 검사에서의 상태 공간 폭발을 해결하기 위해 Kofola 는 결과 SGRA 를 위한 새로운 온더플라이 공집합성 검사 알고리즘을 사용합니다.

• 게으른 구성 (Lazy Construction): 전체 곱 오토마타의 명시적 구성을 요구하는 도구들과 달리, Kofola 는 상태 공간을 게으르게 탐색합니다.
• 알고리즘: 이 알고리즘은 $Fin$ 술어를 확장한 Couvreur 알고리즘의 변형입니다. 이는 SCC 를 감지하기 위해 전이 집합의 스택을 관리하는 깊이 우선 탐색을 수행합니다.
• 종료: 탐색된 상태 공간이 결과를 결정하기에 충분해지자마자 (수용 사이클을 찾거나 공집합성을 증명하는 경우) 탐색이 종료됩니다. 이는 보충의 주요 폭발 원인이므로, 생성된 여집합 부분을 최소화하는 데 중요합니다.

주요 기여

1. Kofola 도구: BA 보충 및 언어 포함성 검사를 위한 효율적이고 모듈식인 도구.
2. IADAC 식별: IADAC(Initial Almost Deterministic Accepting Components) 을 뚜렷한 구조적 클래스로서 도입하고 형식화함.
3. 새로운 보충 알고리즘: $Fin(0)$ 조건을 생성하여 단일 일반화 라빈 쌍을 구성할 수 있게 하는 IADAC 를 위한 전용 부분 알고리즘.
4. 게으른 공집합성 검사: 명시적 전체 오토마타 구성을 피하고 조기 종료를 가능하게 하는 SGRAs 를 위한 새로운 온더플라이 알고리즘.
5. 모듈식 프레임워크: 구조적 분석에 기반하여 서로 다른 부분 알고리즘을 동기식으로 결합할 수 있는 유연한 아키텍처.

실험 결과

저자들은 Kofola 를 Spot, Ranker, Owl, Bait, Forklift, Rabit과 같은 최첨단 도구들과 비교 평가했습니다.

보충 벤치마크

• 데이터셋: 프로그램 종료, 슈트링어 단어 논리, 하이퍼속성, S1S, LTL 번역, 그리고 무작위 생성 등 다양한 소스의 31,273 개 오토마타.
• 견고성: Kofola 는 모든 31,273 개의 입력 오토마타를 성공적으로 보충한 유일한 도구였습니다. 다음으로 가장 견고한 도구인 Spot 은 메모리 제한으로 인해 2 개의 인스턴스에서 실패했습니다.
• 크기: Kofola 는 평균적으로 Spot(115.38 개 상태) 과 Ranker(443 개 인스턴스에서 실패했으나 45.80 개 상태) 에 비해 훨씬 더 작은 여집합 오토마타를 생성했습니다 (79.24 개 상태).
• 성능: Kofola 는 가장 많은 인스턴스를 해결했으며, 종종 경쟁사보다 실행 시간에서 여러 자릿수 (orders of magnitude) 더 우수한 성능을 보였습니다.

포함성 검사 벤치마크

• 데이터셋: 프로그램 종료, 동시성 시스템 검증, 하이퍼속성 모델 체킹, 그리고 정리 증명에서 유래한 1,014 개의 포함성 문제.
• 성능: Kofola 는 가장 많은 인스턴스를 해결했습니다 (해결되지 않은 경우 2 개만). 해결된 문제에 대한 총 실행 시간도 가장 낮았습니다 (141 초).
• 비교: Kofola 는 Spot(Det) 에 대해 263 개 인스턴스에서 엄격하게 승리했고, 0 개에서 패배했습니다. Kofola 는 종종 실행 시간을 한 자릿수 더 요구했던 램지 기반 도구들 (Bait, Forklift, Rabit) 보다 크게 우월한 성능을 보였습니다.
• 관찰: 포함성 쿼리의 오른쪽에 있는 오토마타 (보충되는 것들) 의 98% 는 엘리베이터 오토마타 (NAC 를 포함하지 않음) 였으며, 이는 구조적 속성을 활용하는 것의 실용적 관련성을 강조합니다.

중요성과 주장

본 논문은 Kofola 가 BA 보충 및 포함성 검사 분야에서 효율성과 견고성의 새로운 표준을 확립한다고 주장합니다. 그 중요성은 다음과 같습니다:

• 실용성: 고전적 구성을 넘어 실용적인 포함성 검사에 현대적인 분해 기반 보충 기법을 도입합니다.
• 확장성: 구조적 분해와 게으른 온더플라이 공집합성 검사를 결합함으로써 상태 공간 폭발을 효과적으로 완화하여 기존 도구로는 해결 불가능한 인스턴스를 해결합니다.
• 확장 가능성: 모듈식 아키텍처는 특정 구성 요소 유형을 위한 새로운 부분 보충 알고리즘의 통합을 허용합니다.

저자들은 Kofola 를 단순한 점진적 개선이 아닌, 실용적 응용에서 유래한 벤치마크에서 최첨단 솔루션보다 종종 여러 자릿수 더 우수한 성능을 보이는 매우 경쟁력 있는 도구로 위치시킵니다.