Skip to main content

On the undecidability of asynchronous session subtyping

Lange, Julien and Yoshida, N. (2017) On the undecidability of asynchronous session subtyping. In: Esparza, J. and Murawski, A., eds. Foundations of Software Science and Computation Structures. FoSSaCS 2017. Lecture Notes in Computer Science, 10203 (10203). Springer, Berlin, Germany, pp. 441-457. ISBN 978-3-662-54457-0. E-ISBN 978-3-662-54458-7. (doi:10.1007/978-3-662-54458-7_26) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) (KAR id:62265)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided. (Contact us about this Publication)
Official URL
http://dx.doi.org/10.1007/978-3-662-54458-7_26

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 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.

Item Type: Book section
DOI/Identification number: 10.1007/978-3-662-54458-7_26
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Divisions: Faculties > Sciences > School of Computing
Depositing User: Julien Lange
Date Deposited: 12 Jul 2017 14:36 UTC
Last Modified: 28 Jan 2020 12:58 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/62265 (The current URI for this page, for reference purposes)
Lange, Julien: https://orcid.org/0000-0001-9697-1378
  • Depositors only (login required):