Hennessy-Milner Logic in CSLib, the Lean Computer Science Library

논문 요약: Lean 컴퓨터 과학 라이브러리 (CSLib) 내의 Hennessy–Milner 논리 형식화

1. 문제 제기 (Problem)

• 배경: 레이블 전이 시스템 (LTS, Labelled Transition Systems) 은 프로세스 계산, 통신 프로토콜, 자동화 및 반응형 시스템 등 다양한 계산 시스템의 운영적 행동을 정의하는 표준 프레임워크입니다. 이러한 시스템을 분석하기 위한 핵심 논리인 **Hennessy–Milner 논리 (HML)**는 중요한 기초를 제공합니다.
• 핵심 정리: HML 의 가장 중요한 특징은 Hennessy–Milner 정리입니다. 이는 이미지 유한 (image-finite) LTS 에 대해, 두 상태가 정확히 동일한 HML 명제를 만족할 때와 두 상태가 강력히 동형 (strongly bisimilar) 일 때 동치임을 보장합니다.
• 현황 및 한계: HML 의 이론적 중요성에도 불구하고, **라이브러리 수준의 일반성 (library-grade generality)**을 갖춘 기계화된 형식화는 매우 부족합니다. 기존 형식화들은 대부분 HML 의 특정 변형이나 특정 종류의 LTS 에 국한되어 있어, 다양한 시스템에 재사용하기 어렵습니다.
• 목표: Lean 증명 보조기 (Theorem Prover) 의 커뮤니티 프로젝트인 **CSLib (Lean Computer Science Library)**에 HML 을 범용적이고 재사용 가능한 라이브러리 수준으로 통합하여, 자동화 및 검증 소프트웨어 개발의 기초를 마련하는 것입니다.

2. 방법론 (Methodology)

이 연구는 Lean 4 를 사용하여 HML 의 문법, 만족 관계, 의미론 및 메타이론을 CSLib 인프라에 통합하는 방식으로 진행되었습니다.

• 범용성 (Parametricity): 정의는 임의의 상태 (State) 와 레이블 (Label) 타입에 대해 매개변수화 (universe-polymorphic) 되어 있어, 특정 시스템에 종속되지 않습니다.
• CSLib 인프라 통합:
  • CSLib 의 기존 LTS 구조 (LTS State Label) 와 이산 (Bisimilarity) 정의에 직접 호환되도록 설계되었습니다.
  • Lean 의 수학 라이브러리인 Mathlib 의 집합론 도구를 활용하여 의미론을 구현했습니다.
• 자동화 활용: 증명 과정에서 Lean 의 강력한 자동화 전략인 grind 태크틱을 적극 활용하여, 집합 연산과 정의 전개에 따른 복잡한 증명 단계를 자동으로 처리했습니다.
• 논리 체계:
  • 문법: true, false, 논리 연산자 (∧, ∨), 그리고 모달 연산자 (⟨µ⟩ 다이아몬드, [µ] 박스) 를 포함하는 귀납적 타입 (Inductive Type) 으로 정의되었습니다. (부정 연산자는 false 와 ∧, ∨ 를 통해 유도되는 방식으로 처리하여 만족 관계의 정의를 단순화했습니다.)
  • 의미론: 귀납적 만족 관계 (Satisfies relation, s |= φ) 와 구성적 의미론 (Denotational semantics, 각 명제를 만족하는 상태의 집합) 을 모두 정의하고 두 개념의 동치성을 증명했습니다.

3. 주요 기여 (Key Contributions)

1. 범용 HML 형식화: 문법, 만족 관계, 의미론을 포함하는 HML 의 완전한 라이브러리 수준 형식화를 Lean 에 구현했습니다.
2. 완전한 메타이론 증명:
   • 의미론의 정확성: 귀납적 만족 관계와 구성적 의미론이 동치임을 증명했습니다.
   • 동형 불변성 (Bisimulation Invariance): 동형인 상태는 논리적으로 구별할 수 없음을 증명했습니다.
   • Hennessy–Milner 정리: 이미지 유한 LTS 에 대해, **이론 동치 (Theory Equivalence)**와 **동형 (Bisimilarity)**이 일치함을 증명했습니다. 이는 HML 의 가장 핵심적인 메타이론적 결과입니다.
3. CSLib 통합 및 API 제공:
   • CSLib 의 기존 모듈 (예: 자동화 이론, 통신 시스템 계산 CCS) 과 직접 호환되도록 설계되었습니다.
   • 하위 프로젝트에서 HML 을 즉시 적용할 수 있는 적절한 API 와 문서를 제공했습니다.
4. 공유 및 재현성: 모든 소스 코드는 CSLib 저장소에 공개되었으며, Lean 4.28.0-rc1 버전으로 검증되었습니다.

4. 결과 (Results)

• 자동화된 증명: grind 태크틱을 통해 대부분의 증명 (특히 집합 연산과 정의 전개가 필요한 경우) 을 자동으로 성공적으로 수행했습니다. 이는 수동 증명의 번거로움을 줄이고 신뢰성을 높였습니다.
• 실제 적용 사례:
  • CSLib 에 정의된 **CCS (Calculus of Communicating Systems)**와 자동화 이론에 HML 을 직접 적용하여, 해당 시스템의 동형 관계가 HML 의 이론 동치와 일치함을 확인했습니다.
  • 이미지 유한성 조건 (예: 가드된 재귀 사용) 하에서 CCS 프로세스에 대한 Hennessy–Milner 정리가 성립함을 보였습니다.
• 논리적 동치성: 두 상태가 동형일 때와 두 상태가 만족하는 명제의 집합 (이론) 이 같을 때를 동치로 증명함으로써, HML 이 LTS 의 구조적 동치성을 완벽하게 포착함을 입증했습니다.

5. 의의 및 중요성 (Significance)

• 라이브러리 표준의 확립: CSLib 내의 첫 번째 모달 논리 형식화로서, 향후 CSLib 내에서의 확장 및 응용을 위한 기준 구현체 (Reference Implementation) 역할을 합니다.
• 재사용성과 확장성: 특정 시스템에 종속되지 않는 범용적인 설계로 인해, 다양한 계산 모델 (프로세스 계산, 통신 프로토콜 등) 에 HML 을 쉽게 적용할 수 있는 토대를 마련했습니다.
• 미래 연구의 기반:
  • 현재는 강한 동형 (Strong Bisimilarity) 과 이미지 유한 LTS 에 초점을 맞추었으나, 약한 동형 (Weak Equivalences) 이나 고정점 연산자 (Fixpoint operators) 로의 확장을 위한 기반을 제공했습니다.
  • π-계산 (π-calculus) 과 같은 변수 이름에 의존하는 시스템으로의 확장을 위한 논의의 출발점이 되었습니다.
• 검증 소프트웨어 개발: 형식화된 메타이론을 통해 검증된 소프트웨어 및 시스템 개발의 신뢰성을 높이는 데 기여합니다.

결론적으로, 이 논문은 Hennessy–Milner 논리의 이론적 깊이를 유지하면서도 Lean 과 CSLib 의 현대적인 자동화 및 모듈화 기능을 활용하여, 컴퓨터 과학 연구와 검증 소프트웨어 개발에 즉시 활용 가능한 강력한 도구를 제공했습니다.