Nondeterministic Probabilistic Petri Net -- A New Method to Study Qualitative and Quantitative Behaviors of System  

作　　者：Yang Liu Huai-Kou Miao Hong-Wei Zeng Yan Ma Pan Liu 

机构地区：[1]School of Computer Engineering and Science, Shanghai University, Shanghai 200072, China [2]School of Information Science and Technology, Taishan University, Taian 271021, China [3]State Key Laboratory of Novel Software Technology, Nanjing University, Nanjing 210093, China

出　　处：《Journal of Computer Science & Technology》2013年第1期203-216,共14页计算机科学技术学报（英文版）

基　　金：This work was supported by the National Natural Science Foundation of China under Grant Nos. 60970007, 61073050 and 61170044, the National Basic Research 973 Program of China under Grant No. 2007CB310800, the Shanghai Leading Academic Discipline Project of China under Grant No. J50103, and the Natural Science Foundation of Shandong Province of China under Grant No. ZR2012FQ013.

摘　　要：There are many variants of Petri net at present, and some of them can be used to model system with both function and performance specification, such as stochastic Petri net, generalized stochastic Petri net and probabilistic Petri net. In this paper, we utilize extended Petri net to address the issue of modeling and verifying system with probability and nondeterminism besides function aspects. Using probabilistic Petri net as reference, we propose a new mixed model NPPN （Nondeterministic Probabilistic Petri Net） system, which can model and verify systems with qualitative and quantitative behaviours. Then we develop a kind of process algebra for NPPN system to interpret its algebraic semantics, and an action- based PCTL （Probabilistic Computation Tree Logic） to interpret its logical semantics. Afterwards we present the rules for compositional operation of NPPN system based on NPPN system process algebra, and the model checking algorithm based on the action-based PCTL. In order to put the NPPN system into practice, we develop a friendly and visual tool for modeling, analyzing, simulating, and verifying NPPN system using action-based PCTL. The usefulness and effectiveness of the NPPN system are illustrated by modeling and model checking an elaborate model of travel arrangements workflow.There are many variants of Petri net at present, and some of them can be used to model system with both function and performance specification, such as stochastic Petri net, generalized stochastic Petri net and probabilistic Petri net. In this paper, we utilize extended Petri net to address the issue of modeling and verifying system with probability and nondeterminism besides function aspects. Using probabilistic Petri net as reference, we propose a new mixed model NPPN （Nondeterministic Probabilistic Petri Net） system, which can model and verify systems with qualitative and quantitative behaviours. Then we develop a kind of process algebra for NPPN system to interpret its algebraic semantics, and an action- based PCTL （Probabilistic Computation Tree Logic） to interpret its logical semantics. Afterwards we present the rules for compositional operation of NPPN system based on NPPN system process algebra, and the model checking algorithm based on the action-based PCTL. In order to put the NPPN system into practice, we develop a friendly and visual tool for modeling, analyzing, simulating, and verifying NPPN system using action-based PCTL. The usefulness and effectiveness of the NPPN system are illustrated by modeling and model checking an elaborate model of travel arrangements workflow.

关 键 词：NONDETERMINISM probabilistic Petri net model checking action-based probabilistic computation tree logic 

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