On the undecidability of asynchronous session subtyping

Abstract

Asynchronous session subtyping has been studied extensively in [9, 10, 29{32] and applied in [24, 33, 34, 36]. An open question was whether this subtyping relation is decidable. This paper settles the question in the negative. To prove this result, we rst introduce a new subclass of two-party communicating nite-state machines (CFSMs), called asynchronous duplex (ADs), which we show to be Turing complete. Secondly, 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 checking whether two CFSMs are in the relation. In addition, we show the compatibility relation to be decidable for three sub-classes of ADs.