초록

용어보기논문에서 용어와 풀이말을 자동 추출한 결과로, 시범 서비스 중입니다. AI-Helper

본 연구에서는 만족성 검사기를 이용하여 두 유한 상태 기계의 행위가 동치인지를 검사한다. 기존의 동치 검사는 대부분 BDD를 기반으로 했었기 때문에 변수 순서 배열 및 내부 BDD노드 폭발 문제에 시달렸었다. 하지만 여기서는 BDD대신 명제 논리를 이용하기 때문에 위와 같은 문제점을 피할 수 있다. 하지만 논리식을 만족성 검사기의 입력 형태인 논리곱 정규형으로 변환하는 과정에서 절의 3기는 식의 크기에 지수적으로 증가하였다.

본 연구에서는 만족성 검사기를 이용하여 두 유한 상태 기계의 행위가 동치인지를 검사한다. 기존의 동치 검사는 대부분 BDD를 기반으로 했었기 때문에 변수 순서 배열 및 내부 BDD노드 폭발 문제에 시달렸었다. 하지만 여기서는 BDD대신 명제 논리를 이용하기 때문에 위와 같은 문제점을 피할 수 있다. 하지만 논리식을 만족성 검사기의 입력 형태인 논리곱 정규형으로 변환하는 과정에서 절의 3기는 식의 크기에 지수적으로 증가하였다.

AI 본문요약

엑셀 다운로드 AI-Helper

* AI 자동 식별 결과로 적합하지 않은 문장이 있을 수 있으니, 이용에 유의하시기 바랍니다.

• 연구 주제
• 연구 방법
• 연구 결과

문제 정의

• 지금 까지는 모밸 M 을 논리식으로 만드는 부분올 살펴 보았 다. 동치 조건인 속성 ♦롤 논리식으로 표현하는 부분에 대해서 살 펴보자.
• 모델M 이 논리식으로 표현되는 방법에 대해서 살펴보자.
• 본 연구에서는 유한 상태 기계의 동치 검사를 만족성 검사기로 해결하는 방법을 제시하고 구현을 통하여 확인하였다. 검사될 두 기계를 DT 를 통해서 표현 하였고, DT 의 연산으로 모델 M 과 동 치조건올 나타내는 속성 8의 논리식을 만들었다.
• 여제폴 통해 만족성 검사기를 통한 동치 검사의 수행 결과를 살펴보자.
• 지금부터는 모델이 속성을 만족하는지(M 切 8) 롤 통해 동치 검사를 수행하는 방범에 대해서 살펴보자.

가설 설정

• 유한 상태 기계를 나타내는 논리식에서 모델M, 속성 8의 논리식 을 보다 쉽게 유도하기 위해 새로운 자료 구조를 정 의 한다. 정의 2: 자료 구조 DT(Decision Tree)는 (卩, E)로 구성 된다.
• 정의 8: 상태에 대한 현재 표현과 다옴 표현온 다음처럼 변경이 가 능하다.

제안 방법

• 본 연구에서는 유한 상태 기계의 동치 검사를 만족성 검사기로 해결하는 방법을 제시하고 구현을 통하여 확인하였다. 검사될 두 기계를 DT 를 통해서 표현 하였고, DT 의 연산으로 모델 M 과 동 치조건올 나타내는 속성 8의 논리식을 만들었다. 그런 후, 동치 검 사를 수행하기 위해, 도寻 가눙한 모든 천이가 속성 $에 대해서 만족 가능한 해석이 존재하는지를 만족성 검사기를 뤃해 수행하였으며, 시스템의 구현을 통해서 자동화하였다.
• 동치 검사는 도달성 분석으로 수행할 수 있다. 검사할 유한 상 태 기 계 MA/ Mb 로부터 곱 기 계 M = Ma X Mb 을 구축한 후 초기 상태로부터 도달 가능한 상태를 방문하면서 그때마다 모든 입력 에 대해서 두 기계의 출력이 같은지를 검사한다. 한편, 모델 검사 도구를 이용하여 동치 검사를 할 수 있다 [2].
• 겅의 엇 만족성 검사기롤 사용하여 동치 검사룔 수행하기 위해서 초기 상태 Init 와 속성 $의 현재 상태로 표현 논리식을 다음 상태로 표현된 논리식으로 변경한다.
• 먼저 유한 상태 기계를 새로 정의 한 자료구조로 표현하고, 이들의 연산을 통해 모델 M = Ma xMb 의 논리식과 두 기계의 동치 조건인 속성 8를 논리식으로 표현한다. 그런 후, 기존 만족성 검사 도구인 JSAT(Th으 Java SATisfiability Library, ⑶)를 이용하여 만족 가능한 해사1 이 있는지 검사한다. 초기 상태로부터 도달 가능한 모든 천이의 논리식 이 동치 조건의 논리식에 대해 만족 가능한 해석이 존재하는지 여부를 통해 동치 또눈 비 동치를 결정한다.
• 검사될 두 기계를 DT 를 통해서 표현 하였고, DT 의 연산으로 모델 M 과 동 치조건올 나타내는 속성 8의 논리식을 만들었다. 그런 후, 동치 검 사를 수행하기 위해, 도寻 가눙한 모든 천이가 속성 $에 대해서 만족 가능한 해석이 존재하는지를 만족성 검사기를 뤃해 수행하였으며, 시스템의 구현을 통해서 자동화하였다. 여러 예제에 시스템을 적용해 본 결과 동치 여부의 결과는 정확하였고, 수행 시간 도 효율적이었으나, 검사할 천이를 논리곱 정규형으로 변환하는 과정에 식의 크기에 지수에 해당하는 절수의 결과가 나타났다.
• 본 논문에서는 기존의 동치 검사와는 달리 만족성 검사기플 이용하여 동치 검사를 수행한다. 먼저 유한 상태 기계를 새로 정의 한 자료구조로 표현하고, 이들의 연산을 통해 모델 M = Ma xMb 의 논리식과 두 기계의 동치 조건인 속성 8를 논리식으로 표현한다. 그런 후, 기존 만족성 검사 도구인 JSAT(Th으 Java SATisfiability Library, ⑶)를 이용하여 만족 가능한 해사1 이 있는지 검사한다.
• 본 논문에서는 기존의 동치 검사와는 달리 만족성 검사기플 이용하여 동치 검사를 수행한다. 먼저 유한 상태 기계를 새로 정의 한 자료구조로 표현하고, 이들의 연산을 통해 모델 M = Ma xMb 의 논리식과 두 기계의 동치 조건인 속성 8를 논리식으로 표현한다.
• 본 연구에서는 동치 검사 문제를 回등의 기존 연구에 비해서 BDDs가 아닌 만족성 검사기를 통하여 수행하였다. 본 연구와 관련해서 앞으로 계속 연구해야 할 내용은 다음과 같다.
• 둘째, 기존의 만족성 검사기를 이용한 방법[3 6]들과의 비교 연구이다. 셋째, 만족성 검사기를 이용하여 유한 상태 기계 보다 표현력이 높은 상태도에 대해서 동치 검사를 수행하는 것이다.

이론/모형

• 기존 만족성 검사기 JSAT 온 DIMACS 형식으로 입력 받아서, 만족성 또는 불만족성을 결정한다. 따라서, 만족성 여부를 검사할 논리곱 정규형온 DIMACS 형식으로 변환한다.

성능/효과

• 그런 후, 동치 검 사를 수행하기 위해, 도寻 가눙한 모든 천이가 속성 $에 대해서 만족 가능한 해석이 존재하는지를 만족성 검사기를 뤃해 수행하였으며, 시스템의 구현을 통해서 자동화하였다. 여러 예제에 시스템을 적용해 본 결과 동치 여부의 결과는 정확하였고, 수행 시간 도 효율적이었으나, 검사할 천이를 논리곱 정규형으로 변환하는 과정에 식의 크기에 지수에 해당하는 절수의 결과가 나타났다. 이 것은 커다란 시스템 검증을 방해하는 주요한 요인이다.

본문요약 정보가 도움이 되었나요? 예 아니오 제출

이 논문을 인용한 문헌

더보기