Non-deterministic transducer models of retransmission protocols over noisy channels

• We propose non-deterministic transducer models of retransmission protocols.
• We give the verification methodology for these protocol models.
• We establish decidability for two expressive cases of models.
• The verification is decidable even if the message lengths are unbounded.
• Our technique models key aspects of HDLC and TCP protocols over noisy channels.

Retransmission protocols such as HDLC and TCP are designed to ensure reliable communication over noisy channels (i.e., channels that can corrupt messages). Thakkar et al. [15] have recently presented an algorithmic verification technique for deterministic streaming string transducer (DSST) models of such protocols. The verification problem is posed as equivalence checking between the specification and protocol DSSTs. In this paper, we argue that more general models need to be obtained using non-deterministic streaming string transducers (NSSTs). However, equivalence checking is undecidable for NSSTs. We present two classes where the models belong to a sub-class of NSSTs for which it is decidable.