Reversible process calculi, such as \(\mathtt{\textbf{roll}}\text {-}\pi \) , can accommodate fault-tolerant communication protocols. However, untyped process calculi cannot guarantee desirable behavioural properties such as deadlock-freedom. Concomitantly, Multiparty Session Types (MPST) can provide such guarantees by construction, but often do not consider failures. This suggests that, by leveraging both MPST and \(\mathtt{\textbf{roll}}\text {-}\pi \) , we can facilitate the representation of failures without requiring a significant extension to the MPST theory. However, \(\mathtt{\textbf{roll}}\text {-}\pi \)  lacks choice and replication primitives, which are key features for an MPST-based type system. Nonetheless, its expressiveness allows these constructs to be encoded directly. In this paper, we introduce \(\mathtt{\textbf{roll}}\text {-}\pi !\oplus \) , a variant of \(\mathtt{\textbf{roll}}\text {-}\pi \)  that incorporates choice and replication, and outline its encoding in \(\mathtt{\textbf{roll}}\text {-}\pi \) . This extension lays the foundation for integrating \(\mathtt{\textbf{roll}}\text {-}\pi \)  with MPST.

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

Encoding Choice and Replication in  \(\mathtt{\textbf{roll}}\text {-}\pi \)

  • Adam D. Barwell,
  • Ping Hou,
  • Martin Vassor,
  • Nobuko Yoshida

摘要

Reversible process calculi, such as \(\mathtt{\textbf{roll}}\text {-}\pi \) , can accommodate fault-tolerant communication protocols. However, untyped process calculi cannot guarantee desirable behavioural properties such as deadlock-freedom. Concomitantly, Multiparty Session Types (MPST) can provide such guarantees by construction, but often do not consider failures. This suggests that, by leveraging both MPST and \(\mathtt{\textbf{roll}}\text {-}\pi \) , we can facilitate the representation of failures without requiring a significant extension to the MPST theory. However, \(\mathtt{\textbf{roll}}\text {-}\pi \)  lacks choice and replication primitives, which are key features for an MPST-based type system. Nonetheless, its expressiveness allows these constructs to be encoded directly. In this paper, we introduce \(\mathtt{\textbf{roll}}\text {-}\pi !\oplus \) , a variant of \(\mathtt{\textbf{roll}}\text {-}\pi \)  that incorporates choice and replication, and outline its encoding in \(\mathtt{\textbf{roll}}\text {-}\pi \) . This extension lays the foundation for integrating \(\mathtt{\textbf{roll}}\text {-}\pi \)  with MPST.