Taking Complete Finite Prefixes To High Level, Symbolically

이 논문은 **고수준 페트리 넷 (High-level Petri Nets)**의 **기호적 전개 (Symbolic Unfolding)**에 대해 **완전 유한 접두사 (Complete Finite Prefixes)**를 정의하고, 이를 구성하는 알고리즘을 제안하며, 이를 통해 모델 검증 문제를 해결하는 방법을 다룹니다. 저자들은 기존 P/T (Place/Transition) 페트리 넷의 전개 이론을 고수준 넷으로 확장하고, 무한한 도달 가능 상태 (reachable markings) 를 가진 넷까지 범위를 넓힌 새로운 접근법을 제시합니다.

다음은 논문의 상세 기술 요약입니다.

1. 문제 정의 (Problem)

• 배경: 페트리 넷은 분산 시스템을 모델링하는 데 널리 사용되지만, 상태 폭발 (state explosion) 문제로 인해 대규모 시스템의 검증이 어렵습니다. 이를 해결하기 위해 P/T 페트리 넷의 **전개 (Unfolding)**와 완전 유한 접두사 (Complete Finite Prefix) 개념이 개발되었습니다.
• 한계:
  • 고수준 페트리 넷 (Colored Petri Nets): 다양한 색 (color) 을 가진 토큰을 처리할 수 있어 표현력이 뛰어나지만, 이를 P/T 넷으로 확장 (Expansion) 하면 상태 공간이 기하급수적으로 커져 기존 알고리즘 적용이 비효율적이거나 불가능합니다.
  • 무한 상태 공간: 기존 P/T 넷의 완전 유한 접두사 알고리즘 (예: ERV 알고리즘) 은 도달 가능한 상태의 수가 유한할 때만 작동합니다. 고수준 넷은 무한한 색 집합을 가질 수 있어 도달 가능 상태가 무한한 경우가 많으며, 이 경우 기존 알고리즘은 적용되지 않거나 무한히 실행됩니다.
  • 기호적 전개 (Symbolic Unfolding): 고수준 넷의 행동을 직접적으로 표현하는 '기호적 전개'는 존재하지만, 이를 효율적으로 잘라내어 (cut-off) 유한한 접두사를 만드는 체계적인 방법론이 부족했습니다.

2. 방법론 (Methodology)

저자들은 P/T 넷의 완전 유한 접두사 이론을 고수준 넷의 기호적 수준으로 끌어올리는 다음과 같은 방법론을 제시합니다.

2.1. 개념 확장 및 정의

• 완전 접두사 (Complete Prefix) 의 고수준 정의: 고수준 넷의 기호적 전개에서, 모든 도달 가능한 마킹 (marking) 을 나타내고 모든 전이 (transition) 의 발화 가능성을 보장하는 접두사를 정의합니다.
• 적절 순서 (Adequate Order) 의 일반화: 구성 (configuration) 간의 순서를 정의하여 알고리즘이 최소한의 접두사를 생성하도록 유도합니다.
• Cut-off Event (절단 이벤트) 의 새로운 기준:
  • 기존 P/T 넷에서는 특정 이벤트의 미래가 이미 관찰된 마킹과 일치할 때 절단합니다.
  • 고수준 넷에서는 **마킹의 집합 (Set of Markings)**을 비교합니다. 즉, 현재 이벤트 $e$의 Cone Configuration 이 생성하는 모든 마킹 집합 $M([e])$이 이전에 관찰된 모든 마킹 집합의 합집합에 포함될 때 절단합니다.

2.2. 알고리즘: 일반화된 ERV 알고리즘

• Esparza, Römer, Vogler (ERV) 의 알고리즘을 고수준 넷에 맞게 수정한 **Generalized ERV-Algorithm (Alg. 1)**을 제안합니다.
• 입력: 안전 (Safe) 하고 도달 가능 상태가 유한한 고수준 넷 (Class $N_F$).
• 작동 원리: 가능한 확장 (Possible Extensions) 을 생성하고, '적절 순서'에 따라 이벤트를 추가하며, 새로운 '절단 기준'을 적용하여 불필요한 분기를 제거합니다.
• 보장: 이 알고리즘은 유한한 완전 접두사를 생성하며, P/T 넷을 고수준 넷으로 해석했을 때 기존 ERV 알고리즘과 동일한 결과를 도출합니다.

2.3. 무한 상태 공간 처리: 기호적으로 컴팩트한 넷 (Symbolically Compact Nets)

• 도달 가능 상태가 무한한 경우 (Class $N_{SC}$) 에는 기존 절단 기준이 무한 반복을 초래할 수 있음을 발견했습니다.
• 해결책: 도달 가능한 모든 마킹을 도달하는 데 필요한 전이 발화 횟수에 상한 (bound) 이 존재하는 '기호적으로 컴팩트한 넷'을 정의하고, Cut-off (Cut-off Star)* 기준을 도입했습니다.
  • 이는 특정 이벤트의 Cone Configuration 뿐만 아니라, 순서상 더 작은 모든 구성 (Configuration) 의 마킹 집합과 비교하여 절단 여부를 판단합니다.
  • 기호적 표현 (Symbolic Representation): 무한한 마킹 집합을 직접 저장하지 않고, **제약 조건 (Constraints)**과 **SMT 솔버 (CVC5)**를 사용하여 논리적 포함 관계를 검증함으로써 유한 시간 내에 절단 여부를 결정합니다.

3. 주요 기여 (Key Contributions)

1. 이론적 통합: 고수준 페트리 넷의 기호적 전개와 완전 유한 접두사 개념을 통합하여, P/T 넷 이론을 고수준으로 자연스럽게 확장했습니다.
2. 알고리즘 개발: 안전하고 도달 가능 상태가 유한한 고수준 넷을 위한 일반화된 ERV 알고리즘을 제안했습니다.
3. 무한 상태 처리: 도달 가능 상태가 무한하지만 '기호적으로 컴팩트'한 넷에 대해 작동하는 새로운 절단 기준 (Cut-off*) 과 기호적 검증 방법을 제시했습니다. 이는 기존에 P/T 넷으로 확장할 수 없었던 넷에 대해 완전한 접두사를 구성할 수 있게 합니다.
4. 모드 결정성 (Mode-determinism) 발견: 고수준 넷의 성능을 예측하는 지표로 '모드 결정성'을 정의했습니다.
   • 모드 결정적 (Mode-deterministic): 모든 상태에서 각 전이가 최대 하나의 모드 (firing mode) 로만 발화 가능한 경우. 이 경우 기호적 접근이 저수준 (P/T) 접근보다 이점이 적습니다.
   • 모드 비결정적 (Mode-nondeterministic): 여러 모드가 가능한 경우. 이 경우 기호적 전개가 상태 공간을 압축하여 저수준 접근보다 훨씬 효율적입니다.

4. 실험 결과 (Results)

저자들은 COLORUNFOLDER라는 프로토타입 구현체를 개발하여 4 가지 새로운 벤치마크 패밀리 (Fork And Join, Water Pouring Puzzle, Hobbits And Orcs, Mastermind) 에 대해 실험을 수행했습니다.

• Fork And Join (높은 비결정성):
  • 색상 수 ($m$) 와 장소 수 ($n$) 가 증가할 때, 저수준 접근은 시간이 기하급수적으로 증가하여 5 분 타임아웃을 기록했습니다.
  • 반면, 기호적 접근은 색상 수에 무관하게 약 200ms 내에 결과를 도출했습니다.
• Water Pouring Puzzle (모드 결정적):
  • 이 문제는 모드 결정적이어서 기호적 전개와 저수준 전개 구조가 유사합니다.
  • 실험 결과, 저수준 접근이 더 빠른 경우가 많았으며, 기호적 접근의 이점이 크지 않았습니다.
• Hobbits And Orcs (매개변수 의존적):
  • 보트 용량이 작을수록 (모드 결정성 높음) 저수준이 유리했으나, 용량이 커질수록 (비결정성 증가) 기호적 접근이 우위를 점했습니다.
• Mastermind (코드 깨기 게임):
  • 색상 수 ($m$) 가 증가할 때 저수준 접근은 상태 폭발로 인해 실패했으나, 기호적 접근은 일정한 성능을 유지했습니다.
  • 코드 길이 ($n$) 가 증가할 때 두 방법 모두 시간이 증가했으나, 기호적 접근의 접두사 크기 (노드 수) 는 선형적으로 증가하는 반면 저수준은 기하급수적으로 증가했습니다.

5. 의의 및 결론 (Significance)

• 효율성 증대: 고수준 페트리 넷의 모델 검증에서 상태 폭발 문제를 해결하기 위해, P/T 넷으로의 확장 없이 직접 기호적 수준에서 완전 유한 접두사를 구성할 수 있음을 입증했습니다.
• 범용성 확장: 무한한 도달 가능 상태를 가진 넷 (기존에는 처리 불가) 에 대해서도 기호적으로 컴팩트한 조건 하에 완전한 분석이 가능함을 보였습니다.
• 실용적 가이드: '모드 결정성'이라는 새로운 개념을 통해, 언제 기호적 접근이 저수준 접근보다 유리한지 예측할 수 있는 기준을 제시했습니다.
• 미래 전망: 기호적 도달 가능 그래프 (Symbolic Reachability Graph) 구축, $k$-bounded 넷으로의 일반화, 그리고 고수준 페트리 게임 (Petri Games) 에 대한 전략 분석 등으로 연구 범위를 확장할 수 있음을 시사합니다.

이 논문은 분산 시스템 검증 분야에서 고수준 모델링의 잠재력을 최대한 활용하면서도 계산적 효율성을 보장하는 강력한 이론적, 실용적 기반을 마련했습니다.