π-calculus, Session Types research at the University of Oxford
Systems of communicating automata are prominent models for peer-to-peer message-passing over unbounded channels, but in the general scenario, most verification properties are undecidable. To address this issue, two decidable subclasses, Realisable with Synchronous Communication (rsc) and k-Multiparty Compatibility (k-mc), were proposed in the literature, with corresponding verification tools developed and applied in practice. Unfortunately, both rsc and k-mc are not resilient under failures: (1) their decidability relies on the assumption of perfect channels and (2) most standard protocols do not satisfy rsc or k-mc under failures. To address these limitations, this paper studies the resilience of rsc and k-mc under two distinct failure models: interference and crash-stop failures. For interference, we relax the conditions of rsc and k-mc and prove that the inclusions of these relaxed properties remain decidable under interference, preserving their known complexity bounds. We then propose a novel crash-handling communicating system that captures wider behaviours than existing multiparty session types (MPST) with crash-stop failures. We study a translation of MPST with crash-stop failures into this system integrating rsc and k-mc properties, and establish their decidability results. Finally, by verifying representative protocols from the literature using rsc and k-mc tools extended to interferences, we evaluate the relaxed systems and demonstrate their resilience.
@inproceedings{SY2025,
author = {Amrita Suresh and Nobuko Yoshida},
title = {{Unreliability in Practical Subclasses of Communicating Systems}},
booktitle = {45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Rajasthan, India},
pages = {--},
year = 2025
}
@inproceedings{SY2025,
author = {Amrita Suresh and Nobuko Yoshida},
title = {{Unreliability in Practical Subclasses of Communicating Systems}},
booktitle = {45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Rajasthan, India},
pages = {--},
year = 2025
}