Property analysis of logic Petri nets by marking reachability graphs  

作　　者：Yuyue DU Yuhui NING 

机构地区：[1]College of Information Science and Engineering, Shandong University of Science and Technology, Qingdao 266590, China

出　　处：《Frontiers of Computer Science》2014年第4期684-692,共9页中国计算机科学前沿（英文版）

基　　金：This work is supported by the National Basic Research Program of China （2010CB328101）; the National Natural Science Foundation of China （Grant Nos. 61170078 and 61173042）; the Doctoral Program of Higher Education of the Specialized Research Fund of China （20113718110004）; Basic Research Program of Qingdao City of China （13- 1-4-116-jch）; and the SDUST Research Fund of China （2011KYTD 102）.

摘　　要：Logic Petri nets （LPNs） are suitable to describe and analyze batch processing functions and passing value indeterminacy in cooperative systems. To investigate the dynamic properties of LPNs directly, a new method for analyzing LPNs is proposed based on marking reachability graphs in this paper. Enabled conditions of transitions are obtained and a marking reachability graph is constructed. All reach- able markings can be obtained based on the graph; the fairness and reversibility of LPNs are analyzed. Moreover, the computing complexity of the enabled conditions and reachable markings can be reduced by this method. The advantages of the proposed method are illustrated by examples and analysis.Logic Petri nets （LPNs） are suitable to describe and analyze batch processing functions and passing value indeterminacy in cooperative systems. To investigate the dynamic properties of LPNs directly, a new method for analyzing LPNs is proposed based on marking reachability graphs in this paper. Enabled conditions of transitions are obtained and a marking reachability graph is constructed. All reach- able markings can be obtained based on the graph; the fairness and reversibility of LPNs are analyzed. Moreover, the computing complexity of the enabled conditions and reachable markings can be reduced by this method. The advantages of the proposed method are illustrated by examples and analysis.

关 键 词：logic Petri nets enabled condition reachable marking graph FAIRNESS REVERSIBILITY 

分 类 号：TP393[自动化与计算机技术—计算机应用技术] N02[自动化与计算机技术—计算机科学与技术]