MobilityReadingGroup

On the Undecidability of Asynchronous Session Subtyping

Julien LANGE, Nobuko YOSHIDA

Asynchronous session subtyping has been studied extensively in [8,9,28–31] and applied in [23,32,33,35]. An open question was whether this subtyping relation is decidable. This paper settles the question 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. 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 checking whether two CFSMs are in the relation reduces to the halting problem for Turing machines. In addition, we show the compatibility relation to be decidable for three sub-classes of ADs.

@inproceedings{LY2017,
  author = {Julien Lange and Nobuko Yoshida},
  title = {{On the Undecidability of Asynchronous Session Subtyping}},
  booktitle = {20th International Conference on Foundations of Software Science and Computation Structures},
  series = {LNCS},
  volume = {10203},
  pages = {441--457},
  publisher = {Springer},
  year = 2017
}

@inproceedings{LY2017,
  author = {Julien Lange and Nobuko Yoshida},
  title = {{On the Undecidability of Asynchronous Session Subtyping}},
  booktitle = {20th International Conference on Foundations of Software Science and Computation Structures},
  series = {LNCS},
  volume = {10203},
  pages = {441--457},
  publisher = {Springer},
  doi = "10.1007/978-3-662-54458-7_26",
  year = 2017
}