公开(公告)号：KR100248377B1

公开(公告)日：2000-03-15

申请号：KR1019970053452

申请日：1997-10-17

Applicant: 한국전자통신연구원

Inventor： 정연대 ,  정철주 ,  김영찬

IPC: G06F11/00

Abstract: 본 발명은 액션 집합의 크기가 1인 경우에 한하여 두 개의 병행 시스템의 명세들 간의 완전 트레이스 동치성(completed trace equivalence)을 검사하는 방법에 관한 것이다. 본 발명을 달성하기 위해 두 개의 병행 시스템의 각 명세의 시작 상태에 대하여 특징 함수 (characteristic polynomial)를 생성한 후, 그 각 특징 함수들이 동일한지를 비교함으로써, 두 명세가 완전 트레이스 동치인지를 검사할 수 있는 것이다. 이와 같이 본 발명에서는 다항 함수를 두 개의 배열을 통해 나타내는 방법을 이용함으로써 효율적인 동치성 검사가 이루어지도록 한다. 따라서, 본 발명은 주어진 시스템 명세에서 사용되는 액션 집합의 크기가 1인 경우 두 명세간의 완전 트레이스 동치성을 제곱 시간(quadratic time) 내에 검사해 주게 된다.

公开(公告)号：KR1019990032411A

公开(公告)日：1999-05-15

申请号：KR1019970053452

申请日：1997-10-17

Applicant: 한국전자통신연구원

Inventor： 정연대 ,  정철주 ,  김영찬

IPC: G06F11/00

Abstract: 본 발명은 액션 집합의 크기가 1인 경우에 한하여 두 개의 병행 시스템의 명세들 간의 완전 트레이스 동치성(completed trace equivalence)을 검사하는 방법에 관한 것이다. 본 발명을 달성하기 위해 두 개의 병행 시스템의 각 명세의 시작 상태에 대하여 특징 함수 (characteristic polynomial)를 생성한 후, 그 각 특징 함수들이 동일한지를 비교함으로써, 두 명세가 완전 트레이스 동치인지를 검사할 수 있는 것이다. 이와 같이 본 발명에서는 다항 함수를 두 개의 배열을 통해 나타내는 방법을 이용함으로써 효율적인 동치성 검사가 이루어지도록 한다. 따라서, 본 발명은 주어진 시스템 명세에서 사용되는 액션 집합의 크기가 1인 경우 두 명세간의 완전 트레이스 동치성을 제곱 시간(quadratic time) 내에 검사해 주게 된다.