2026-07-24T17:44:04Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:25131 2026-02-09T08:06:35Z ddc:004 open_access

Unreliability in Practical Subclasses of Communicating Systems Suresh, Amrita Yoshida, Nobuko Communicating automata lossy channel corruption out of order session types crash-stop failure 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Amrita Suresh and Nobuko Yoshida 2025 Is Part Of LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2025.52 urn:nbn:de:0030-drops-251312 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.52 eng https://creativecommons.org/licenses/by/4.0/legalcode