核心概念
이 논문은 동기식 이진 세션 유형의 하위 유형 검사를 위한 세 가지 알고리즘을 제시하고 그 복잡성을 분석한다. 첫 번째 알고리즘은 원래 논문의 귀납적 트리 검색 기반 알고리즘이며, 두 번째 알고리즘은 이를 최적화한 버전이다. 마지막으로 새로운 이차 알고리즘을 제안하는데, 이는 최근에 소개된 X Y Z W-시뮬레이션 개념을 사용한 그래프 검색에 기반한다.
要約
이 논문은 동기식 세션 유형 시스템에서의 하위 유형 검사 알고리즘을 다룬다.
첫 번째로, 원래 논문의 알고리즘의 복잡성을 분석한다. 이 알고리즘은 귀납적 트리 검색에 기반한다. 이 알고리즘의 최악 경우 복잡도는 O(n^3)이다.
두 번째로, 이 알고리즘의 최적화된 버전을 소개한다. 이 버전은 복잡도를 개선했지만 여전히 두 유형의 크기에 대해 지수적이다.
마지막으로, X Y Z W-시뮬레이션 개념을 사용하여 새로운 이차 알고리즘을 제안한다. 이 알고리즘은 유형을 레이블 전이 시스템으로 표현하고 시뮬레이션 관계 검사를 통해 하위 유형을 결정한다. 이 알고리즘의 복잡도는 O(n^2)이다.
統計
두 유형의 크기 n = |T| + |U|일 때, 첫 번째 알고리즘의 최악 경우 복잡도는 O(n^3)이다.
두 번째 알고리즘의 최악 경우 복잡도는 2^O(n^2)이다.
세 번째 알고리즘의 복잡도는 O(n^2)이다.
引用
"세션 유형은 동시 프로세스의 통신 동작을 설명하고 지정하기 위한 유형 규율이다."
"하위 유형은 세션 프로그램의 타입화 가능성을 확장하는 데 널리 사용된다."