Unreliability in practical subclasses of communicating systems

Conference item

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.

Authors: Suresh, A; Yoshida, N

• Publication status: Accepted
• Peer review status: Peer reviewed
• Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
• Acceptance date: 2025-09-15
• Event title: 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)
• Event location: Goa, India
• Event website: https://www.fsttcs.org.in/2025/index.php
• Event start date: 2025-12-17
• Event end date: 2025-12-19
• Language: English
• Keywords: communicating automata; lossy channel; corruption; out of order; session types; crash-stop failure