On the undecidability of asynchronous session subtyping

Asynchronous session subtyping has been studied extensively in [9, 10, 28–31] and applied in [23, 32, 33, 35]. An open question was whether this subtyping relation is decidable. This paper settles the ques- tion in the negative. To prove this result, we first introduce a new sub- class of two-party communicating finite-state machines (CFSMs), called asynchronous duplex (ADs), which we show to be Turing complete. Sec- ondly, we give a compatibility relation over CFSMs, which is sound and complete wrt. safety for ADs, and is equivalent to the asynchronous subtyping. Then we show that the halting problem reduces to check- ing whether two CFSMs are in the relation. In addition, we show the compatibility relation to be decidable for three sub-classes of ADs