Session types are a type discipline for describing and specifying communication behaviours of concurrent processes. Session subtyping, firstly introduced by Gay and Hole, is widely used for enlarging typability of session programs. This paper gives the complexity analysis of three algorithms for subtyping of synchronous binary session types. First, we analyse the complexity of the algorithm from the original paper, which is based on an inductive tree search. We then introduce its optimised version, which improves the complexity, but is still exponential against the size of the two types. Finally, we propose a new quadratic algorithm based on a graph search using the concept of $\mathcal{XYZW}$-simulation, recently introduced by Silva et al.

翻译：会话类型是一种用于描述和规范并发进程间通信行为的类型体系。会话子类型化由Gay和Hole首次提出，被广泛用于扩大会话程序的可类型化能力。本文对同步二进制会话类型子类型化的三种算法进行了复杂度分析。首先，我们分析了原始论文中基于归纳树搜索的算法复杂度；其次，引入其优化版本，该版本虽改进了复杂度，但仍随两种类型的大小呈指数增长；最后，我们提出一种新的二次算法，该算法基于图搜索并采用了Silva等人最近引入的$\mathcal{XYZW}$-仿真概念。