A Topological Framework for Finite Behavioural Observations and Verification

당신이 로봇이나 소프트웨어 프로그램 같은 복잡한 기계를 이해하려고 노력하고 있다고 상상해 보십시오. 하지만 당신은 그 내부의 기어나 코드를 볼 수 없습니다. 오직 그 기계가 무엇을 하는지만 관찰할 수 있을 뿐입니다. 이 논문은 우리가 이러한 제한적인, 즉 "유한한(finite)" 행동의 단편들을 사용하여 기계가 제대로 작동하고 있는지 어떻게 알아낼 수 있는지에 관한 것입니다.

저자인 안토니스 아킬레오스(Antonis Achilleos)와 바실리키 키리아쿠(Vasiliki Kyriakou)는 관찰한 것들을 조직하기 위한 거대한 지도로서 위상수학(topology)(모양과 공간을 연구하는 수학의 한 분야)을 사용합니다. 여기서의 위상수학은 고무판이 아니라, 우리가 볼 수 있는 것을 바탕으로 사물들을 "이웃(neighborhoods)"으로 분류하는 방법이라고 생각하십시오.

다음은 그들의 연구 결과를 쉬운 개념들로 나누어 설명한 이야기입니다.

1. 문제: 나무가 아닌 숲을 보는 것

컴퓨터 과학에서 우리는 종종 시스템이 "좋은지" 검증하고 싶어 합니다. 하지만 우리는 시스템을 영원히 지켜볼 수 없습니다. 우리는 오직 유한한 관찰(finite observations), 즉 시스템이 수행하는 동작의 짧은 영상만을 얻을 수 있습니다.

• 비유: 영화의 줄거리를 단 5초의 클립만 보고 추측해야 한다고 상상해 보십시오. 만약 자동차 추격전을 본다면, 그 영화에 액션이 있다는 것을 알 수 있습니다. 하지만 자동차 한 대만 본다면, 그것이 주행 중인지, 주차 중인지, 아니면 충돌 중인지 알 수 없습니다.

논문은 다음과 같이 질문합니다: 우리가 이 짧은 클립들을 보는 것만으로 어떤 종류의 "진실"을 확인할 수 있는가?

2. 첫 번째 지도: "트레이스(Trace)" 관점 (선형 경로)

기계를 관찰하는 가장 단순한 방법은 단순히 기계가 누르는 버튼의 목록(그것의 "트레이스")을 기록하는 것입니다.

• 비유: 직선으로 걷는 로봇을 상상해 보십시오. 당신은 오직 그것이 남긴 발자국만을 봅니다.
• 발견: 만약 당신이 이 발자국만을 본다면, 당신이 얻게 될 수학적 "지도(위상)"는 **칸토어 위상(Cantor Topology)**입니다. 이것은 사물들이 긴 발자국의 역사를 공유할 때 서로 가깝다고 간주되는, 잘 정돈된 유명한 지도입니다.
• 반전: 만약 당신이 발자국의 전체 무한한 역사를 한꺼번에 보려고 시도한다면(Full Trace Inclusion), 지도는 무너지고 **이산적(discrete)**이 됩니다. 이는 모든 로봇이 각각 고립된 섬이 된다는 것을 의미합니다. 전체 무한한 미래를 일치시켜야 한다는 요구 조건이 너무 엄격하기 때문에 더 이상 서로를 비교할 수 없게 됩니다. 이는 두 사람이 오직 태생부터 죽을 때까지의 삶이 완전히 똑같아야만 "유사하다"고 말하는 것과 같습니다.

3. 두 번째 지도: "시뮬레이션(Simulation)" 관점 (분기 경로)

저자들은 단순히 발자국만 보는 것이 중요한 무언가를 놓치고 있다는 것을 깨달았습니다: 바로 **선택(Choices)**입니다.

• 비유: 두 대의 로봇을 상상해 보십시오.
  • 로봇 A는 복도를 따라 걷다가 갈림길에 도달합니다. 로봇 A는 왼쪽(문으로 연결) 또는 오른쪽(창문으로 연결)으로 갈 수 있습니다.
  • 로봇 B는 똑같은 복도를 따라 걷다가 갈림길에 도달합니다. 로봇 B는 왼쪽(문으로 연결) 그리고 동시에 오른쪽(창문으로 연결)으로 갈 수 있습니다(또는 둘 다 할 수 있는 메커니즘을 가지고 있습니다).
  • 만약 당신이 발자국만을 본다면, 두 로봇은 "걷기, 왼쪽으로 돌기, 멈추기"와 "걷기, 오른쪽으로 돌기, 멈추기"로서 동일하게 보일 것입니다.
• 발견: 저자들은 **$\tau_{sim}$ (시뮬레이션 위상)**이라는 새로운 지도를 도입했습니다. 이 지도는 "유한한 루프 없는 프로세스(finite loop-free processes)"를 관찰 대상으로 사용합니다. 이것들을 작은 선택의 흐름도라고 생각하십시오.
  • 이 새로운 지도는 경로가 아닌 선택의 구조를 보기 때문에 로봇 A와 로봇 B를 구분해 낼 수 있습니다.
  • 결과: 이 지도는 발자국 지도보다 "더 미세합니다(finer)". 즉, 더 작고 구체적인 이웃들을 만들어냅니다.

4. 황금률: 열린 집(Open Sets)은 "검증 가능한 진실"이다

이것이 이 논문의 가장 큰 이론적 돌파구입니다. 그들은 수학과 검증을 연결하는 일반적인 규칙을 증명했습니다:

• 규칙: 어떤 속성(예: "로봇이 안전하다")이 검증 가능하려면, 그것은 그들의 지도 위에서 **"열린 집(open set)"**이어야 합니다.
• 비유: 지도 위의 "안전 구역"을 상상해 보십시오. 만약 그 구역이 "열려" 있다면, 당신이 그 구역 안 어디에 있더라도 작은 발걸음(유한한 관찰)을 통해 여전히 구역 안에 있음을 보장받을 수 있습니다. 당신은 전체 지도를 볼 필요 없이 안전하다는 것을 알 수 있습니다. 짧은 엿보기만으로 충분합니다.
• 만약 어떤 속성이 열린 집이 아니라면, 유한한 클립을 보는 것만으로는 그것이 참인지 결코 100% 확신할 수 없습니다. 당신은 항상 경계선에 서서 다음 순간이 확인해주기를 기다려야 할 수도 있습니다.

5. 규칙 적용하기: 모니터링 가능성(Monitorability)

그들은 이 규칙을 그들의 두 지도에 적용했습니다:

• 발자국 지도($\tau_O$)에서: 검증 가능한 속성들은 몇 가지 특정한 동작의 시퀀스를 관찰함으로써 확인할 수 있는 것들입니다(다중 트레이스 모니터 가능성).
• 선택 지도($\tau_{sim}$)에서: 검증 가능한 속성들은 몇 가지 특정한 선택의 패턴을 관찰함으로써 확인할 수 있는 것들입니다(시뮬레이션 모니터 가능성).

6. "데드락(Deadlock, 교착 상태)"의 놀라움

저자들은 더 엄격한 규칙, 예를 들어 "완전 시뮬레이션(Complete Simulation)"(기계가 작동을 멈추는지, 즉 데드락에 걸리는지 확인하는 것)을 사용하려고 할 때 어떤 일이 발생하는지 테스트했습니다.

• 문제: 그들은 만약 이러한 더 엄격한 규칙을 지도의 기초로 사용하려 한다면, 지도가 무너진다는 것을 발견했습니다. 이 지도는 모든 기계를 포괄하지 못합니다. 어떤 기계들은 영원히 작동하며 결코 "멈추지" 않으므로, 엄격한 "정지 확인" 범주에 들어맞지 않습니다.
• 해결책: 그들은 **유한 깊이 비시뮬레이션(Finite-Depth Bisimulation)**이라는 절충안을 찾아냈습니다. 이것은 정확히 k 단계 동안 두 로봇이 동일하게 행동하는지 확인하는 것과 같습니다.
• 결과: 이것은 **완전히 새로운 지도($\tau_{fin}^{bis}$)**를 만들어냅니다.
  • 핵심 차이점: 이 새로운 지도에서는 "데드락에 걸린(stuck)" 로봇(멈춰서 아무것도 하지 않는 로봇)을 실제로 식별할 수 있습니다. 이전의 "시뮬레이션" 지도에서는, 시뮬레이션이 멈춘 로봇이 모방될 수 있는지 여부만을 체크할 뿐 반드시 모방되어야 하는지를 체크하지 않기 때문에, 멈춘 로봇이 마치 움직이기 직전의 로봇처럼 보였습니다.
  • 이 새로운 지도에서, "멈춰 있음(stuck)"은 눈에 보이는 뚜렷한 특징(열려 있으면서 동시에 닫힌 집, 즉 'clopen' 세트)이 됩니다.

요약

이 논문은 다음과 같은 수학적 프레임워크를 구축합니다:

1. 유한한 관찰(행동의 짧은 클립)은 지도(위상)를 만듭니다.
2. 검증 가능한 속성은 정확히 이 지도 위의 열린 영역입니다.
3. 선택을 관찰하는 것(시뮬레이션)은 단순히 경로를 관찰하는 것보다 더 상세한 지도를 제공합니다.
4. 특정 깊이까지의 선택을 관찰하는 것(비시뮬레이션)은 "멈춘" 기계들을 명확히 보여주는 완전히 다른 지도를 만들어냅니다.

요컨대, 저자들은 우리가 시스템을 "관찰하는" 방식이 우리가 그것을 검증하는 데 사용하는 수학적 풍경을 결정하며, 서로 다른 관찰 방식이 서로 다른 진실을 드러낸다는 것을 보여주었습니다.