본 논문에서는 유한페트리넷의 도달가능성에 대한 효율적인 분석방법을 제안한다. 일반적으로 도달가능성 분석은 유한페트리넷의 동적 성질에 관한 연구에 있어서 가장 근본이 되는 분석중의 하나이다. 그러나 일반적인 유한페트리넷의 경우, 도달가능성 분석은 분석시간과 요구되는 메모리 양의 측면에서 지수승의 복잡도를 요구하게 되며 많은 경우 상태공간폭발 문제를 야기할 수 있다. 이에 본 논문에서는 유한페트리넷의 분석을 위한 중간모델인 언폴딩(unfolding)상에서 장소(place)간의 구조관계 분석을 통하여 시간 및 메모리의 측면에서 효율적으로 도달가능성 분석을 수행하는 방법을 제안한다. 제안된 방법은 구조적 제약 없이 모든 종류의 유한페트리넷에 적용 가능하다.
This paper suggests an efficient reachability analysis method of bounded petri nets. Reachability analysis is a fundamental basis for studying the dynamic properties of any discrete event systems. However, it takes at least exponential execution time and memory space to verify in general petri nets. That is, state space explosion problem may occur. In this paper, we attack problems of previous approaches - state space explosion and restrictions to applicable petri net classes - by formulating the reachability problem as set operation over structural relations among places on an unfolding.
