Abstract
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 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 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.
Cite
CITATION STYLE
Lange, J., & Yoshida, N. (2017). On the undecidability of asynchronous session subtyping. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10203 LNCS, pp. 441–457). Springer Verlag. https://doi.org/10.1007/978-3-662-54458-7_26
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
