In this thesis, three transformation methods of Petri nets to simplify the analysis of Petri net modeled systems are proposed. In the literature, mostly proposed methods need to construct the reachability graph (or the set of all the reachable markings) of the corresponding Petri net for analyzing some characteristics of a system such as safeness, deadlock-freeness and liveness etc. However, constructing the reachability graph of a complicated Petri net requires much time and a large state space. The complexity is known to be at least exponential and may not even be decidable [Lipt76]. So the problem of keeping the exponential growth of the state space of complex Petri net under control is an important issue as this growth may impair the analysis of realistic systems.
To resolve the problem, many researchers have proposed abstraction and refinement methods of the net which are based on the characteristics of the subnet. But their methods are much more fitted to the stepwise refinement of the net since the safeness (boundedness) of the net must be checked first [Suzu83] [Vale79]. In this thesis, at first, a transformation (abstraction) method for simplification of Petri nets which is an extension of Suzuki's work (abstraction of k-well behaved module) is proposed. Convertible subnet (CSN) is defined so that the boundedness of the original net is not to be checked. Furthermore, some transitions in the CSN may have output arcs to the places outside the CSN. This implies that the abstracted module may have interaction outside the module not through the entry or exit points. A complicated Petri net is transformed into a simpler one with a smaller state space by hierarchically replacing a CSN with the corresponding decision net. It is shown that the properties (liveness, boundness etc.) of the original net is not changed during the transformation and an illustrative example of the abstraction is given which is a simple CPU model.
Also to analyze the performance of a system modeled by a timed Petri net, finding the reachability graph of the corresponding timed Petri net is essential. We propose a transformation method for simplification of timed Petri nets to estimate the response time. A timed convertible subnet (TCSN) is defined appropriately to maintain informations such as response time and the probability of meeting a deadline etc. Using the TCSN, a complicated timed Petri net which is live and safe is transformed into a simpler one with a similar method. And an efficient algorithm to find CSN's or TCSN's is also proposed. We show that the information for the response time analysis is not lost but is kept during the transformation. And an example is given with the same CPU model for the response time analysis.
Finally, Petri net based satisfiability testing method for non-clausal propositional calculus is presented. This can be used for the case that a system is modeled by a Petri net and a formula or a specification is given by a predicate logic. Every formula in propositional calculus is hierarchically represented by an acyclic free-choice Petri net called logic Petri net. Then a logic Petri net is combined with two way alternating modules, whose number depends upon the number of atoms used in the formula. It is shown that the satisfiability and the truth set of a formula with non-clausal form can be tested by obtaining reachable firing set of the complete logic Petri net corresponding to the formula under the maximum firing rule.
본 논문은 페트리망으로 모델링된 시스템의 분석을 효율적으로 하기위한 세가지의 페트리망의 변환방법을 제안하고 있다. 기존의 방법들은 시스템의 특성을 분석하기 위하여 페트리망의 도달그래프(Reachabilty Graph)를 구하여야만 하였으나 도달그래프를 구하는 것은 많은 시간과 대규모 상태공간(State Space)을 필요로 하며 이의 복잡도 (Complexity)는 지수함수적으로 증가하는 것으로 알려져 왔다. 따라서 페트리망의 상태공간을 줄이는 것은 대단히 중요한 일이다.
이를 해결하기 위하여 subnet의 특성에 기초한 페트리망의 변환 (Abstraction, Refinement) 방법들이 많이 제안되었다. 그러나 기존의 변환방법들은 시스템의 Boundedness를 점검하여야 하므로 Abstraction보다는 Refinement에 적합하다고 할 수 있다. 본논문에서는 Suzuki의 변환방법을 확장한 방법을 제안하고 있다. 제안된 변환방법은 Boundedness의 점검이 필요하지 않으며, Subnet의 내부가 외부와의 작용이 가능하도록 CSN이 정의되어 있다는 점에서 Suzuki의 방법을 확장하였으며 제안된 방법은 CSN을 순차적으로 그에 대응하는 Decision Net로 대체함으로써 복잡한 페트리망을 작은 상태공간을 가지는 간단한 페트리망으로 변환하게 된다. 또한 CSN을 효과적으로 찾는 알고리즘을 제안하였으며 이 변환방법을 적용하여도 시스템의 특성(Safeness Liveness등)은 변하지 않음을 증명하였고, 간단한 CPU 모델을 이용하여 본 변환방법의 예를 보였다.
또한 시간사양 페트리망으로 모델링된 시스템의 성능분석을 위하여는 시간사양 페트리망의 상태공간을 구하는 것이 필요로 하게 된다. 본논문에서는 두번째로 시간사양 페트리망의 분석을 간단히 하기위한 변환방법을 제안하였으며 시간사양 페트리망을 변환하는동안 응답시간, 성능 추정 등에 필요한 정보가 변하지 않도록 Subnet(TCSN)을 정의하였고 이를 이용하여 복잡한 시간사양 페트리망을 위와 유사한 방법을 이용하여 간단하게 만드는 방법을 제안하였다. 또한 제안된 방법을 이용하여도 시스템의성능을 추정할 수 있음을 증명하였고 간단한 CPU모델을 예로들어 제안된 변환방법이 성능분석에 유용함을 보였다.
마지막으로 본논문에서는 Propositional Calculus에대한 만족해의 존재여부를 페트리망에 기초하여 조사하는 방법을 제안하였다. 이방법은 시스템이 페트리망으로 모델링되고 시스템의 규격이 Propositional Calculus로 주어졌을 경우에 유용하며 시스템의 분석을 일원화할 수 있게 된다. Propositional Calculus의 공식은 Logic 테트리망이라는 비순환 Free-choice 페트리망으로서 순차적으로 표현되며 이것이 Two way alternating module과 결합하게 된다. 이를 이용하여 공식의 만족해의 존재여부와 만족해를 구할 수 있으며 이 문제가 페트리망의 Reachability 문제로 변환될 수 있음을 보였다. 또한 CLPN을 보다 효율적으로 수행하기위하여 Maximum firing rule이 적용될 수 있음을 보였다.
