기술 요약: 벡터의 구간을 이용한 심볼릭 모델 체킹

1. 문제 정의

모델 체킹은 소프트웨어 및 하드웨어 시스템이 명세를 준수하는지 확인하기 위한 강력한 형식 검증 기법이다. 그러나 이는 시스템 크기에 따라 가능한 상태와 전이의 수가 기하급적으로 증가하는 **상태 공간 폭발 문제(state space explosion problem)**에 의해 심각하게 저해된다. 이러한 도전 과제는 단일 구성을 검증하는 것이 아니라, 계산 트리 논리(Computation Tree Logic, CTL) 공식이 만족되는 모든 상태를 식별하는 것을 목표로 하는 **글로벌 모델 체킹(global model checking)**에서 특히 두드러진다.

결정 다이어그램(Decision Diagrams, DDs), 추상화, 부분 순서 감소(partial order reduction)와 같은 기존 기술들은 이를 완화하지만, 모델이 더 정교해짐에 따라 한계에 직면한다. 구체적으로, 표준적인 구간 기반 접근 방식(예: Interval Decision Diagrams)은 벡터의 집합을 **벡터의 구간(vectors of intervals)**으로 인코딩한다. 본 논문은 페트리 넷(Petri nets)의 경우, 벡터의 구간이 아닌 **벡터의 일반화된 구간(generalized intervals on vectors, 즉 구간의 벡터)**을 사용하여 마킹(marking)의 집합을 인코딩하는 것이 더 효과적이라고 주장한다. 이 차이는 벡터 공간이 종종 비전체 부분 순서(non-total partial orders)를 포함하기 때문에, 단순한 구간 정의만으로는 불충분하다는 점에서 매우 중요하다.

2. 방법론

저자들은 페트리 넷 마킹의 집합을 인코딩하기 위해 **심볼릭 벡터 집합(Symbolic Vector Sets, SVS)**이라는 새로운 심볼릭 구조를 제안한다. 이 방법론은 세 가지 핵심 축을 기반으로 구축된다.

2.1. 심볼릭 벡터 및 집합

**심볼릭 벡터(Symbolic Vector)**는 $a$와 $b$가 벡터(마킹)의 집합인 쌍 $(a, b)$로 정의된다.

• 포함 ($a$): 마킹 $q$가 심볼릭 벡터에 속한다는 것은 $q$가 $a$에 있는 모든 벡터를 포함함($\subseteq_f$라는 비엄격 부분 순서 하에)을 의미한다.
• 배제 ($b$): 마킹 $q$가 심볼릭 벡터에 속하지 않는다는 것은 $q$가 $b$에 있는 어떤 벡터도 포함하지 않음을 의미한다.
• 일반화: 이는 자연수의 구간 $[a, b]$ (여기서 $a \le x \le b$)를 벡터로 일반화한 것이다. 벡터는 항상 비교 가능한 것이 아니므로, 이 구조는 단일 경계 대신 하한 집합($a$)과 상한 집합($b$)을 필요로 한다.

**심볼릭 벡터 집합(Symbolic Vector Set)**은 이러한 심볼릭 벡터들의 모임이며, 그 기저에 있는 마킹 집합들의 합집합을 나타낸다.

2.2. 정규형(Canonical Form) 및 연산

효율성을 보장하고 중복을 피하기 위해, 저자들은 심볼릭 벡터 및 집합에 대한 **정규형(canonical form)**을 정의한다. 주요 속성은 다음과 같다:

• 유일성: 모든 마킹 집합은 정확히 하나의 정규 표현을 갖는다.
• 준동형 연산(Homomorphic Operations): 본 논문은 개별 마킹으로 디코딩하지 않고 심볼릭 구조에서 직접 작동하는 준동형 연산(합집합, 교집합, 차집합, 부정)을 정의한다.
• 병합 가능성 및 공유 가능성: 정규성을 유지하기 위해, 저자들은 두 심볼릭 벡터를 병합할 수 있는지 또는 "공유 가능한(shareable)" 구성 요소가 존재하는지를 결정하는 관계를 도입한다. 이는 비전체 부분 순서에서의 모호성을 해결하기 위해 렉시코그래픽 전체 순서(lexicographic total order)를 사용하여, 겹치는 제약 조건을 결정론적으로 처리한다.

2.3. 페트리 넷에 대한 CTL 모델 체킹

이 프레임워크는 유한 용량을 가진 페트리 넷에 이 구조들을 적용한다.

• Pre-연산: 글로벌 모델 체킹의 핵심은 선행 마킹(predecessor markings)을 계산하는 pre 연산이다. 저자들은 전이의 가역성과 용량 제약을 처리하며 심볼릭 벡터 집합에서 작동하는 심볼릭 pre 연산을 정의한다.
• 고정점 평가(Fixpoint Evaluation): CTL 공식(예: $EF, EG, EU$)은 심볼릭 벡터 집합에 대한 고정점 계산(최소 및 최대 고정점)을 사용하여 평가된다. 공식의 만족 여부는 마킹이 결과 심볼릭 벡터 집합에 속하는지 확인하여 결정된다.

2.4. 최적화

• 포화(Saturation): 고정점 계산 중 중간 솔루션이 불필요하게 커지는 "피크 효과(peak effect)"를 해결하기 위해, 저자들은 포화 전략을 구현한다. 이는 용량 경계를 반복하고 이전 결과를 활용하여 후속 단계를 계산함으로써, 중간 심볼릭 벡터의 수를 크게 줄인다.
• 클러스터링(Clustering): 논문은 도달 가능성(reachability)을 위한 최적화로서 작은 벡터들을 결합하는 클러스터링을 언급하지만, 이는 향로의 공식적 기술을 위한 개념으로 남겨두었다.

3. 주요 기여

1. 새로운 인코딩: 벡터의 비전체 부분 순서를 처리하기 위해 특별히 설계된, 구간을 벡터로 일반화한 구조인 심볼릭 벡터 집합을 도입하였다.
2. 형식적 정규화: 유일성에 대한 증명과 정규성을 보존하는 준동형 연산(합집합, 교집합, 차집합, 부정)을 포함하여, 심볼릭 벡터 및 집합에 대한 정규형을 엄밀하게 정의하였다.
3. 글로벌 모델 체킹 프레임워크: 이러한 심볼릭 구조를 사용하여 페트리 넷에서 CTL 공식을 평가하기 위한 완전한 형식주의를 포함하여, 심볼릭 pre 연산의 정의를 제공하였다.
4. 포화 알고리즘: 고정점 반복 과정 중의 계산적 피크를 완화하기 위해 심볼릭 벡터 집합의 맥락에서 포화 원리를 적용하였다.
5. 구현 (SVSKit): 이론을 구현한 Swift 라이브러리인 SVSKit을 개발하였으며, 이를 Model Checking Contest (MCC) 2022 벤치마크로 테스트하였다.

4. 결과

저자들은 MCC 2022의 예시, 특히 Circadian Clock 모델을 사용하여 SVSKit 도구의 성능을 평가하였다.

• 포화에 따른 확장성: Circadian Clock 모델에 대한 실험 결과, 포화가 필수적임이 입증되었다. 포화 없이 계산 시간은 용량에 따라 기하급수적으로 증가했다(용량 6에서 5시간 초과). 반면, 포화를 적용하면 용량이 2 이상일 때 계산 시간이 일정하게 유지되었으며(약 3.2초), 심볼릭 벡터의 수도 안정적이었다.
• 대규모 상태 공간 처리: 도구는 용량이 $N=100,000$인 경우에도 성공적으로 처리하였으며, 약 $10^{84}$개의 마킹을 단 26개의 심볼릭 벡터로 인코딩하였다.
• 벤치마크 성능: MCC 2022의 CTL fireability 카테고리에서, 기존 도구들(GreatSPN, ITS-Tools, Tapaal)은 60분의 제한 시간 내에 16개 쿼리를 모두 답변하는 데 실패했다(Tapaal은 9/16 답변). SVSKit 방식은 16개 쿼리를 모두 약 30분 만에 해결하였다.
• 한계: 저자들은 현재 구현이 정규 연산의 최악 복잡도($O(n!)$)로 인해 확장성 문제를 겪고 있음을 인정하였다. 효율성은 이러한 연산의 구현에 크게 의존하며, 벤치마크의 경우 이러한 제약으로 인해 상대적으로 작은 페트리 넷으로 제한되었다.

5. 의의 및 주장

본 논문은 "벡터의 구간"에서 "구간의 벡터"로의 전환을 통해 기존의 심볼릭 모델 체킹 기술에 대한 유망한 대안을 제시한다고 주장한다.

• 이론적 기여: 벡터 집합을 부분 순서 하에서 조작하기 위한 형식적 대수 프레임워크를 제공하여, 이러한 구조가 정체되어 있던 문헌의 공백을 메운다(30년 전의 원형인 "Predicate structures"를 참조).
• 실용적 타당성: 실험 결과는 이 접근 방식이 명시적 열거보다 훨씬 더 큰 상태 공간을 더 효율적으로 처리할 수 있으며, 특히 큰 용량을 포함하는 특정 글로벌 모델 체킹 작업에서 현재의 도구들을 능가할 잠재력이 있음을 시사한다.
• 향후 방향: 저자들은 현재 구현이 최적화, 특히 정규 연산의 최적화가 필요함을 겸허히 인정한다. 향후 연구로는 로컬 모델 체킹으로의 확장, 페트리 넷 너머의 모델로의 확장, 그리고 결정 다이어그램과의 통합을 제안하며, 두 접근 방식은 서로 직교하며 하이브리드화의 이점을 얻을 수 있다고 기술한다.

결론적으로, 본 논문은 현재의 구현에 한계가 있음에도 불구하고, 심볼릭 벡터 집합이 글로벌 모델 체킹을 위한 잠재력을 가지고 있음을 이론적 토대와 초기 실험 결과를 통해 입증하였다.