http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
- 中文 을 입력하시려면 zhongwen을 입력하시고 space를누르시면됩니다.
- 北京 을 입력하시려면 beijing을 입력하시고 space를 누르시면 됩니다.
RISS 인기검색어
- 검색키워드
- 저자 : Mohammad Esmail Esmaili (검색결과 2 건)
- 무료
- 기관 내 무료
- 유료
-
Improved Region-Based TCTL Model Checking of Time Petri Nets
Mohammad Esmail Esmaili,Reza Entezari-Maleki,Ali Movaghar 한국정보과학회 2015 Journal of Computing Science and Engineering Vol.9 No.1
The most important challenge in the region-based abstraction method as an approach to compute the state space of time Petri Nets (TPNs) for model checking is that the method results in a huge number of regions, causing a state explosion problem. Thus, region-based abstraction methods are not appropriate for use in developing practical tools. To address this limitation, this paper applies a modification to the basic region abstraction method to be used specially for computing the state space of TPN models, so that the number of regions becomes smaller than that of the situations in which the current methods are applied. The proposed approach is based on the special features of TPN that helps us to construct suitable and small region graphs that preserve the time properties of TPN. To achieve this, we use TPN-TCTL as a timed extension of CTL for specifying a subset of properties in TPN models. Then, for model checking TPN-TCTL properties on TPN models, CTL model checking is used on TPN models by translating TPN-TCTL to the equivalent CTL. Finally, we compare our proposed method with the current region-based abstraction methods proposed for TPN models in terms of the size of the resulting region graph.
-
Improved Region-Based TCTL Model Checking of Time Petri Nets
Esmaili, Mohammad Esmail,Entezari-Maleki, Reza,Movaghar, Ali Korean Institute of Information Scientists and Eng 2015 Journal of Computing Science and Engineering Vol.9 No.1
The most important challenge in the region-based abstraction method as an approach to compute the state space of time Petri Nets (TPNs) for model checking is that the method results in a huge number of regions, causing a state explosion problem. Thus, region-based abstraction methods are not appropriate for use in developing practical tools. To address this limitation, this paper applies a modification to the basic region abstraction method to be used specially for computing the state space of TPN models, so that the number of regions becomes smaller than that of the situations in which the current methods are applied. The proposed approach is based on the special features of TPN that helps us to construct suitable and small region graphs that preserve the time properties of TPN. To achieve this, we use TPN-TCTL as a timed extension of CTL for specifying a subset of properties in TPN models. Then, for model checking TPN-TCTL properties on TPN models, CTL model checking is used on TPN models by translating TPN-TCTL to the equivalent CTL. Finally, we compare our proposed method with the current region-based abstraction methods proposed for TPN models in terms of the size of the resulting region graph.
연관 검색어 추천
이 검색어로 많이 본 자료
활용도 높은 자료
