성능 모델에 대한 형식 추론

이산 사건 시뮬레이션(Discrete-event simulation)은 컴퓨터 시스템, 네트워크 및 서비스의 성능을 모델링하고 분석하는 표준 기술입니다. 시뮬레이션 도구가 널리 사용됨에도 불구하고, 이들이 구현하는 모델의 정확성 및 성능 보장에 대한 추론은 여전히 상당 부분 임시방편적(ad hoc)입니다: 시뮬레이션 출력은 통계적으로 해석되지만, 그 동작에 대한 연역적 추론을 위한 논리적 기반이 없습니다. 우리는 이산 사건 시뮬레이터에서 공통적으로 사용되는 필수 구성 요소들—비동기 실행(asynchronous execution), 분포로부터의 연속 및 이산 샘플링(continuous and discrete sampling from distributions), 그리고 전역 이벤트 큐를 통한 시간 기반 이벤트 스케줄링(time-based event scheduling through a global event queue)—을 포착하는 핵심 명령 계산(core imperative calculus)을 제시합니다. 이 계산 위에, 우리는 거의 확실한 도달 가능성(almost-sure reachability) 및 기대 도달 시간 속성(expected reaching time properties)에 대한 추론을 위한 증명 시스템을 개발합니다. 우리의 주요 결과는 이러한 속성에 대한 건전하고 완전한(sound and complete) 증명 규칙입니다. 우리의 프레임워크는 연속 시간과 연속 확률 분포가 핵심인 성능 모델의 설정으로 이산 시간 확률 프로그램에 대한 연역적 추론을 일반화합니다. 우리는 Lean에 내장된 도구에 이러한 증명 규칙을 구현했습니다. 우리는 큐잉 이론(queueing theory)의 해석적 해답을 넘어서는 클라이언트-서버 예제를 포함하여, 네트워크 라우팅 프로토콜의 수렴 거동을 포함한 여러 사례 연구에 대해 거의 확실한 도달 가능성과 기대 도달 시간에 대한 증명을 도출함으로써 우리의 증명 규칙의 적용 가능성을 시연합니다. 우리의 증명 규칙의 건전성과 완전성을 확립하는 것은 이산 시간 설정보다 훨씬 더 복잡한 논증을 필요로 합니다. 이는 운영 의미론(operational semantics)의 근본적으로 불연속적인 특성과 연속 시간 및 확률 분포의 측도 이론적 어려움 때문입니다.