TY - GEN
T1 - Encoding choice and replication in roll-π
AU - Barwell, Adam David
AU - Hou, Ping
AU - Vassor, Martin
AU - Yoshida, Nobuko
N1 - Funding: This research was partially funded by EPSRC EP/T006544/2, EP/N027833/2, EP/N028201/1, EP/T014709/2, EP/Y005244/1, EP/V000462/1,
EP/X015955/1, Horizon EU TaRDIS 101093006.
PY - 2025
Y1 - 2025
N2 - Reversible process calculi, such as roll-π, 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 roll-π, we can facilitate the representation of failures without requiring a significant extension to the MPST theory. However, roll-π 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 pa- per, we introduce roll-π!⊕, a variant of roll-π that incorporates choice and replication, and outline its encoding in roll-π. This extension lays the foundation for integrating roll-π with MPST.
AB - Reversible process calculi, such as roll-π, 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 roll-π, we can facilitate the representation of failures without requiring a significant extension to the MPST theory. However, roll-π 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 pa- per, we introduce roll-π!⊕, a variant of roll-π that incorporates choice and replication, and outline its encoding in roll-π. This extension lays the foundation for integrating roll-π with MPST.
KW - Reversible process calculus
KW - Causally consistent rollback
KW - Multiparty session types
KW - Fault-tolerance
U2 - 10.1007/978-3-031-97063-4_3
DO - 10.1007/978-3-031-97063-4_3
M3 - Conference contribution
SN - 9783031970627
T3 - Lecture Notes in Computer Science
SP - 27
EP - 36
BT - Reversible computation
A2 - Glück, Robert
A2 - Kaarsgaard, Robin
PB - Springer
CY - Cham
ER -