Nondeterministic Probabilistic Petri Net — A New Method to Study Qualitative and Quantitative Behaviors of System
Nondeterministic Probabilistic Petri Net — A New Method to Study Qualitative and Quantitative Behaviors of System
复制标题
DOI：
10.1007/s11390-013-1323-7
复制
发表时间：
2013-02
影响因子：
0.7
通讯作者：
Yang Liu;Huai-kou Miao;Hong-wei Zeng;Yan Ma;Pan Liu
中科院分区：
文献类型：
--
作者：
Yang Liu;Huai-kou Miao;Hong-wei Zeng;Yan Ma;Pan Liu
目前Petri网有多种变体，其中一些可以用来对功能和性能规范的系统进行建模，例如随机Petri网、广义随机Petri网和概率Petri网。在本文中，我们利用扩展Petri网来解决除了函数方面之外的概率和非确定性系统的建模和验证问题。以概率Petri网为参考，我们提出了一种新的混合模型NPPN（非确定性概率Petri网）系统，它可以对具有定性和定量行为的系统进行建模和验证。然后我们为NPPN系统开发一种过程代数来解释其代数语义，并开发一种基于动作的PCTL（概率计算树逻辑）来解释其逻辑语义。随后我们提出了基于NPPN系统过程代数的NPPN系统组合运算规则，以及基于动作的PCTL的模型检验算法。为了将 NPPN 系统付诸实践，我们开发了一个友好的可视化工具，使用基于动作的 PCTL 来建模、分析、模拟和验证 NPPN 系统。通过对旅行安排工作流程的精细模型进行建模和模型检查，说明了 NPPN 系统的实用性和有效性。
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.