분산 시스템은 점점 더 무작위화(randomisation)에 의존하고 있지만, 이러한 시스템을 위한 검증 기법은 이를 구축하는 데 사용되는 프로그래밍 추상화와 여전히 분리되어 있습니다. 본 논문은 일반적인 다자 세션 타입(multiparty session types)의 최초 확률적 확장 버전을 제안합니다. 이는 전역 사양 없이 세션을 바텀업(bottom-up) 방식으로 타이핑하며, 오직 세션 타입만으로 다자 세션의 정량적 속성(quantitative properties)을 도출합니다.
저희 타입은 데이터 의존적 제어(data-dependent control)를 추상화하는 확률적 선택(probabilistic choice)과 비결정적 선택(nondeterministic choice)을 결합하며, 선택이나 분기(branching)의 각 분기가 다른 참여자를 포함할 수 있는 분리된 선택을 허용합니다. 이는 이전의 확률적 다자 세션 타입 시스템을 넘어서는 조합입니다.
이를 달성하기 위해, 저희는 새로운 확률적 서브타이핑 관계(probabilistic subtyping relation)와 병합 연산자(merge operator)를 개발했으며, 이를 사용하여 타입 건전성(type soundness)과 세션 충실도(session fidelity)를 증명합니다. 타이핑 컨텍스트의 의미론은 비결정적 해상(nondeterministic resolution), 확률적 선택, 그리고 동기화(synchronisation)를 분리하여, 모든 타이핑 컨텍스트가 유한 마르코프 결정 과정(finite Markov decision process)을 유도하도록 합니다.
이 과정에서, 저희는 모든 공정한 적대적 스케줄러(fair adversarial scheduler) 하에서도 세션이 교착 상태가 아닐 확률(deadlock-free) 및 살아있을 확률(live)에 대한 건전한 하한 경계(sound lower bounds)를 도출합니다. 이는 확률적 세션 계산법(probabilistic session calculus)에서 부분적이거나 아니더라도 최초의 행동 속성 보장입니다.
세션 타입과 확률적 모델 검사(probabilistic model checking)를 연결하기 위해, 저희는 세션 타입을 PRISM 모델링 언어로 변환하는 최초의 방법을 도입하고, 이를 운영 의미론(operational semantics)에 대해 건전하고 완전함을 증명합니다. 이 프레임워크는 Prose 툴체인에 구현되었으며, 이는 확률적 다자 세션 타이핑 컨텍스트를 PRISM으로 변환하여 안전성(safety), 교착 상태 없음(deadlock-freedom), 그리고 활성도(liveness)를 검사합니다.