추상화를 통한 모델의 축소:네모라이즈 게임 사례 연구
Model Reduction with Abstraction: Case Study with Nemorize Game
0
조회
0
다운로드
0
인용
0
참고문헌
키워드
초록
주어진 상태가 도달 가능한지를 판정하는 작업은 모델 체킹과 같은 유한 상태 모델의 분석에서 필수적이다. 만일 모델의 크기가 작다면 상태 공간을 전부 조사해서 판정할 수 있지만, 크기가 큰 경우에는 전체 상태 공간을 조사하는 것이 어렵거나 불가능할 수 있다. 이런 경우, 도달성 여부를 조사하기 전에 추상화를 통해서 모델을 축소해야 하며 이때 사용된 추상화는 false positive 오류를 허용하지 않는다. 본 논문에서는 이러한 추상화를 고안하여 네모라이즈 게임 풀이에 적용하였다. 그 결과, 상태 폭발 문제로 풀 수 없었던 큰 규모의 문제를 추상화를 통해서 해결할 수 있었다.攀※ 본 연구는 한국과학재단 특정기초연구(R01-2005-000-11120-0) 지원으로 수행되었음.†정 회 원：경기대학교 전자계산학과 석사과정††종신회원：경기대학교 정보과학부 교수논문접수：2005년 7월 7일, 심사완료：2005년 12월 13일攀攀
Abstract
Given a state, it is essential to for the finite state model analysis (such as model checking) to decide whether or not the state is reachable. If a size of the model is small, the whole state space is to be explored exhaustively. However, it is very difficult or even impossible if a size of the model is large. In this case, the model can be reduced into a smaller one via abstraction which does not allow the false positive error. In this paper, we devise such an abstraction and apply it to the Nemorize game solving. As a result, unsolved game due to the state explosion problem is solved with the proposed abstraction.
참고문헌 (12)
- "Performance Analysis of Symbolic Reachability Algorithms in Model Checking" (1999)
- "Automatic Abstraction in Model Checking" (2000)
- "Bisimulation and Model Checking", pp.338~341 (1999)
- "Handling Liveness Properties in (ω-)Regular Model-Checking" (2004)
- "Efficient Generation of Counterexamples and Witness in Symbolic Model Checking", pp.427~432 (1995)
- "Applying Model Checking Techniques to Push Push Game Solving", pp.290~303 (2003)
- "Progress on the State Explosion Problem in Model Checking", LNCS 2000, pp.154~169
- "Model Checking" (1999), MIT Press
- "http:", ~kenmcmil, pp.smv
- "http:", spin, pp.whatispin.html#A
- "http:", esterel.org, pp.Html, About[DOI]
- "모델 체킹에서 상태 투영을 이용한 모델의 추상화", 11-D(6), pp.1295~1300 (2004), 한국정보처리학회