On the undecidability of asynchronous session subtyping
File(s)DTRS16-9.pdf (491.16 KB)
Published version
Author(s)
Lange, Julien
Yoshida, Nobuko
Type
Report
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.
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.
Date Issued
2016-01-01
Citation
Departmental Technical Report: 16/9, 2016, pp.1-34
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
34
Journal / Book Title
Departmental Technical Report: 16/9
Copyright Statement
© 2016 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
16/9