SAT 프로시져를 이용한 유한 상태 기계의 동치 검사 = Equivalence Checking Finite State Machines with SAT - Procedure

국문 초록 (Abstract)

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

목차 (Table of Contents)

• 요약
• 1. 서론
• 2. 만족성 검사기를 이용한 동치 검사
• 3. 구현 및 분석
• 4. 결론 및 향후 연구
• 참고문헌