Multiparty session types (MPST) are a robust typing framework that ensures safe and deadlock-free communication within distributed protocols. As these protocols grow in complexity, compositional modeling becomes increasingly important for scalable verification. Therefore, we propose using refinement through subtyping to facilitate the modularity needed for compositional verification. We present a probabilistic extension for MPST with a novel, flexible subtyping system which allows one channel (the interface) to be substituted by several channels (the refinement). Our subtyping is very expressive; any selection of well-typed channels as the refinement has a corresponding interface in a single channel type. To facilitate this generality, we base our system on a powerful variant of MPST, mixed choice multiparty session types, which offers greater flexibility in communication choices.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Compositional Interface Refinement Through Subtyping in Probabilistic Session Types

  • Paula Blechschmidt,
  • Kirstin Peters,
  • Uwe Nestmann

摘要

Multiparty session types (MPST) are a robust typing framework that ensures safe and deadlock-free communication within distributed protocols. As these protocols grow in complexity, compositional modeling becomes increasingly important for scalable verification. Therefore, we propose using refinement through subtyping to facilitate the modularity needed for compositional verification. We present a probabilistic extension for MPST with a novel, flexible subtyping system which allows one channel (the interface) to be substituted by several channels (the refinement). Our subtyping is very expressive; any selection of well-typed channels as the refinement has a corresponding interface in a single channel type. To facilitate this generality, we base our system on a powerful variant of MPST, mixed choice multiparty session types, which offers greater flexibility in communication choices.