A Diagrammatic Axiomatisation of Behavioural Distance of Nondeterministic Processes

Różowski, Piedeleu, Silva, Zanasi 의 논문 "A Diagrammatic Axiomatisation of Behavioural Distance of Nondeterministic Processes"에 대한 상세한 기술적 요약입니다.

1. 문제 제기

이 논문은 비결정적 프로세스의 행동을 정량적으로 비교하는 과제를 다룹니다.

• 배경: 전통적인 프로세스 대수와 오토마타 이론은 동치성 (예: 비시밀라리티, 언어 동치) 에 대한 부울적 개념에 의존합니다. 이는 유용하지만, 확률적이거나 정량적인 측면을 포함하는 현대 시스템에는 너무 경직되어 있으며, 두 행동이 동일한지 여부뿐만 아니라 얼마나 떨어져 있는지를 측정해야 하는 경우가 많습니다.
• 구체적 격차: 행동 거리는 확률적 시스템과 결정적 오토마타 (DFA) 에 대해 연구되어 왔으나, 비결정적 프로세스 (특히 Milner 의 차트) 에 대해서는 타당하고 완전한 공리 체계가 부재합니다.
• 과제: 비결정성은 언어 동치에서 비시밀라리티로 의미론적 초점을 이동시킵니다. 기존 대수적 구문 (바인더가 있는 정규식 등) 은 복잡한 치환 메커니즘 없이 이러한 행동을 구성적으로 포착하는 데 어려움을 겪습니다. 또한, 정량적 추론을 비결정적 시스템으로 확장하려면 "Hausdorff 리프팅"된 거리 측정을 처리해야 하는데, 이를 공리화하는 것은 기술적으로 어렵습니다.

2. 방법론

저자들은 프로세스 행동을 표현하고 추론하기 위해 스트링 다이어그램 (대칭 모노이달 범주의 그래픽 언어) 을 사용하는 도식적 접근법을 채택합니다.

• 의미론적 모델 (차트): 논문은 Milner 의 차트에 초점을 맞추는데, 이는 수용 상태를 변수 출력으로 대체함으로써 유한 상태 비결정적 오토마타 (NFA) 를 일반화합니다. 의미론은 정규 행동 ($\Omega$) 의 범주 위에서 정의되며, 의사거리 구조를 갖습니다.
• 거리 정의: 행동 거리는 코대수적 프레임워크를 통해 정의됩니다. 이는 다음을 활용합니다:
  1. 전이 리프팅: 상태에 대한 거리를 전이 (레이블이 붙은 간선과 변수 출력) 에 대한 거리로 리프팅합니다.
  2. Hausdorff 리프팅: 비결정성을 처리하기 위해 전이 집합으로 거리를 리프팅합니다.
  3. 고정점 특성화: 거리는 의사거리 격자 위의 단조 연산자의 최소 고정점입니다. 이는 비시밀라리티의 계층화 (Hennessy-Milner 논리) 에 의해 구체적으로 특성화되는데, 두 프로세스가 깊이 $n$까지는 비시밀라하지만 $n+1$까지는 그렇지 않다면 거리는 $2^{-n}$입니다.
• 구문 (스트링 다이어그램): 저자들은 구문으로 스트링 다이어그램을 사용합니다. 이 선택은 다음과 같은 이점을 제공합니다:
  • 변수 없는 표현: 재귀는 명시적 바인더와 치환 대신 피드백 루프 (trace) 를 통해 처리됩니다.
  • 구성적 의미론: 다이어그램은 정규 행동의 범주적 구조에 자연스럽게 매핑됩니다.
  • Int 구성: 양방향 데이터 흐름 (입력/출력) 과 피드백 루프를 처리하기 위해, 저자들은 추적된 모노이달 범주를 컴팩트 클로즈드 범주로 변환하는 Int 구성을 사용하여 국소적인 와이어 굽기를 가능하게 합니다.

3. 주요 기여

A. 정량적 추론 시스템

논문은 행동 거리에 대한 상한을 유도하기 위한 정량적 등식 규칙 (추론 시스템) 집합을 제안합니다 ($s \equiv_\epsilon t$).

• 표준 거리 규칙: 반사성, 대칭성, 삼각 부등식, 그리고 "연속성" 규칙 (모든 $\epsilon' > \epsilon$에 대해 $s \equiv_{\epsilon'} t$이면 $s \equiv_\epsilon t$) 이 포함됩니다.
• 구성 규칙: 비확장성을 보존하는 순차 합성과 병렬 합성 (텐서) 에 대한 규칙입니다.
• 도메인 특정 규칙:
  • (Pref): 동작 $a$로 접두사를 붙이면 거리가 절반이 됩니다 ($d(a.s, a.t) = \frac{1}{2}d(s, t)$). 이는 두 프로세스를 구별하는 데 한 단계가 더 필요하다는 직관을 포착합니다.
  • (Codel): 초기 상태가 없는 다이어그램 (데드락) 은 빈 차트와 거리가 0 입니다.
  • 등식 공리: 강한 비시밀라리티 (거리 0) 를 포착하는 공리 집합 (A1-B11) 으로, 비결정적 선택, 변수 병합, 재귀 (Conway 이론 공리) 에 대한 법칙을 포함합니다.

B. 타당성과 완전성

핵심 기술적 성과는 추론 시스템이 타당하고 완전함을 증명하는 것입니다.

• 타당성 (정리 16): 유도 가능한 모든 정량적 등식 $f \equiv_\epsilon g$은 유효합니다 (즉, 실제 행동 거리 $d(\llbracket f \rrbracket, \llbracket g \rrbracket) \leq \epsilon$).
• 완전성 (정리 31): 두 다이어그램 간의 행동 거리가 $\leq \epsilon$이면, 제안된 규칙을 사용하여 등식 $f \equiv_\epsilon g$을 유도할 수 있습니다.
  • 증명 전략: 완전성 증명은 임의의 다이어그램을 정규형 (유한 프리차트를 나타냄) 으로 변환하는 과정을 포함합니다. 그런 다음 추론 규칙을 사용하여 Hausdorff 리프팅 계산과 고정점 반복 (Kleene 의 정리) 을 구문적으로 시뮬레이션합니다. 연속성 (Cont) 규칙은 구문적 근사와 정확한 극한 사이의 간격을 메우는 데 결정적입니다.

C. 범주적 구조

논문은 정규 행동의 범주 ($\text{RegBeh}$) 가 Conway Theory(특정 유형의 추적된 모노이달 범주) 이며, 의사거리 구조가 이를 의사거리 공간의 범주 ($\text{PMet}$) 위에 가장해진 범주로 만든다고 확립합니다. 이는 모든 범주적 연산 (합성, 텐서, trace/dagger) 이 비확장적임을 보장합니다.

4. 결과

• 공식적 특성화: 논문은 Milner 의 차트 (출력이 있는 비결정적 프로세스) 에 대한 행동 거리의 첫 번째 완전한 공리화를 제공합니다.
• 거리의 구문적 시뮬레이션: 저자들은 전이 집합 간의 Hausdorff 거리와 같은 복잡한 거리 계산이 스트링 다이어그램의 구문적 조작을 통해 순수하게 시뮬레이션될 수 있음을 보여줍니다.
• 예시 적용: 논문은 두 개의 특정 차트 (하나는 두 번의 'a' 후 데드락, 다른 하나는 무한한 'a'를 가짐) 가 정확히 $1/4$의 거리에 있음을 증명하는 상세한 유도를 포함합니다. 이는 재귀를 풀고 (Pref) 규칙을 두 번 적용함으로써 달성됩니다.

5. 의의

• 이론과 실전의 연결: 부울 동치에서 정량적 거리로 이동함으로써, "거의 동치"가 의미 있는 개념인 시스템 (예: 근사 시스템 또는 확률적 시스템의 검증) 에 대한 더 세밀한 분석을 가능하게 합니다.
• 통합 도식적 프레임워크: 스트링 다이어그램을 사용하면 전통적인 프로세스 대수에서 발견되는 변수 바인딩과 치환의 복잡성을 피할 수 있습니다. 이는 다양한 계산 모델 (결정적, 비결정적, 확률적, 가중치) 에 대한 동치성과 거리의 공리화를 위한 통합 프레임워크로의 길을 제시합니다.
• 미래 연구의 기초: 이 논문은 행동 거리가 더욱 중요한 가중치 전이 시스템과 확률적 오토마타로 이러한 결과를 확장하기 위한 토대를 마련합니다. 또한 역컴파일 알고리즘과 Guarded Kleene Algebra with Tests (GKAT) 에 대한 추론에 대한 잠재적 응용을 시사합니다.
• 이론적 발전: 코대수적 행동 거리, 정량적 등식 논리, 도식적 대수를 연결하여 프로세스 이론의 오랜 문제를 해결하기 위해 이러한 분야들이 어떻게 통합될 수 있는지를 보여줍니다.

요약하자면, 이 논문은 비결정적 프로세스에 대한 추상적인 코대수적 행동 거리 정의를 구체적이고 도식적이며 완전히 공리화된 계산으로 성공적으로 변환하여, 프로세스 행동에 대한 정량적 추론이 스트링 다이어그램의 구문적 조작을 통해 완전히 수행될 수 있음을 증명합니다.