›› 2013,Vol. 28 ›› Issue (1): 203-216.doi: 10.1007/s11390-013-1323-7

所属专题： Artificial Intelligence and Pattern Recognition

• Special Section on Selected Paper from NPC 2011 • 上一篇    

非确定概率Petri网-一种研究系统定性和定量行为的新方法

Yang Liu1,2,3 (刘阳), Huai-Kou Miao1 (缪淮扣), Senior Member, CCF, Hong-Wei Zeng1 (曾红卫), Yan Ma2 (马艳), and Pan Liu1 (刘攀)   

  • 收稿日期:2011-12-14 修回日期:2012-11-30 出版日期:2013-01-05 发布日期:2013-01-05
  • 基金资助:

    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.

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

Yang Liu1,2,3 (刘阳), Huai-Kou Miao1 (缪淮扣), Senior Member, CCF, Hong-Wei Zeng1 (曾红卫), Yan Ma2 (马艳), and Pan Liu1 (刘攀)   

  1. 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
  • Received:2011-12-14 Revised:2012-11-30 Online:2013-01-05 Published:2013-01-05
  • Supported by:

    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.

PDF (PC)

2525

目前已有多种Petri网模型可以用来对系统功能和性能方面同时建模,例如随机Petri网、广义随机Petri网、概率Petri网等.本文以概率Petri网为参考,扩展经典的Petri网模型用于建模系统的概率和非确定性等方面的特征.首先,在通用网论理论的指导下,以保证非确定性为前提,将概率度量理论引入到经典的Petri网模型,提出了一种非确定概率Petri网模型,给出了其相应的变迁触发规则和结构特征.然后,给出了其进程代数式的语义描述,并研究了基于该语义的非确定概率Petri网的组合运算法则;给出了其时态逻辑层面的语义描述,用action命题扩展PCTL(Probabilistic Computation Tree Logic),定义了一种基于action的PCTL(aPCTL),并给出了aPCTL概率模型检验算法验证非确定概率Petri网系统.基于开源软件PIPE,开发了非确定概率Petri网建模和验证工具NPNMV,并以一个工作流程的实例演示了其概率模型检验过程.

Abstract: 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 actionbased 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.

[1] Girault C, Valk R. Petri Nets for System Engineering: AGuide to Modeling, Verification, and Application. Springer-Verlag, 2003.
[2] Lin C. Stochastic Petri Net and System Performance Evaluation(2nd Edition). Tsinghua University Press, 2005, pp.1-2.(in Chinese)
[3] Noe J D, Nutt G J. Macro e-nets representation of parallelsystems. IEEE Transactions on Computers, 1973, C-22(8):718-727.
[4] Merlin P M, Farber D J. Recoverability of communicationprotocols: Implications of a theoretical study. IEEE Transactionson Communications, 1976, 24(9): 1036-1043.
[5] Molloy M K. On the integration of delay and throughput measuresin distributed processing models [Ph.D. Thesis]. Universityof California, Los Angeles, USA, 1981.
[6] Natkin S. Les reseaux de PETRI stochastiques et leur application`a l’′evaluation des syst`emes informatiques [Ph.D. Thesis].CNAM, Paris, France, 1980. (In French)
[7] Symons F JW. Introduction to numerical Petri nets, a generalgraphical model of concurrent processing systems. AustralianTelecommunications Research, 1980, 14(1): 28-33.
[8] Marsan M A, Conte G, Balbo G. A class of generalizedstochastic Petri nets for the performance evaluation of multiprocessorsystems. ACM Transactions on Computer Systems,1984, 2(2): 93-122.
[9] Petri C A. Introduction to general net theory. In LectureNotes in Computer Science 84, Brauer W (ed.), Springer-Verlag, 1980, pp.1-19.
[10] Balbo G. Introduction to generalized stochastic Petri net. InProc. the 7th Int. Conf. Formal Methods for PerformanceEvaluation, May 2007, pp.83-131.
[11] Baier C, Katoen J P. Principles of Model Checking. MITPress, 2008.
[12] Albanese M, Chellappa R, Moscato V, Picariello A, SubrahmanianV S, Turaga P, Udrea O. A constrained probabilisticPetri net framework for human activity detection in video.IEEE Transactions on Multimedia, 2008, 10(8): 1429-1443.
[13] Kudlek M. Probability in Petri nets. Fundamenta Informaticae— Concurrency Specification and Programming, 2005,67(1/3): 121-130.
[14] Benveniste A, Fabre E, Haar S. Markov nets: Probabilisticmodels for distributed and concurrent systems. IEEE Transactionson Automatic Control, 2003, 48(11): 1936-1950.
[15] Segala R. Modeling and verification of randomized distributedreal-time systems [Ph.D. Thesis]. Massachusetts Institute ofTechnology, Cambridge, USA, 1995.
[16] Yuan C Y. Principle and Application of Petri Net. Beijing:Publishing House of Electronics Industry, 2005, pp.66-78. (inChinese)
[17] Han T T. Diagnosis, synthesis and analysis of probabilisticmodels [Ph.D. Thesis]. RWTH Aachen University, Germany,2009.
[18] Ash R B, Dol′eans-Dade C A. Probability and Measure Theory(2nd edition). Academic Press, 2000, pp.3-10.
[19] Milner R. Communication and Concurrency. Prentice-Hall,1989, pp.10-36.
[20] Hoare C A R. Communicating Sequential Processes. Prentice-Hall, 1985, pp.81-100.
[21] Heljanko K, Junttila T, Latvala T. Incremental and completebounded model checking for full PLTL. In Proc. the 17th InternationalConference on Computer Aided Verification, July2005, pp.98-111.
[22] Hansson H, Jonsson B. A logic for reasoning about time andreliability. Formal Aspects of Computing, 1994, 6(5): 512-535.
[23] Bianco A, de Alfaro L. Model checking of probabilistic andnondeterministic systems. In Proc. the 15th Conference onFoundations of Software Technology and Theoretical ComputerScience, December 1995, pp.499-513.
[24] Emerson E A, Mok A K, Sistla A P, Srinivasan J. Quantitativetemporal reasoning. Real Time Systems, 1992, 4(4):331-352.
[25] Baier C, Katoen J P, Hermanns H. Approximate symbolicmodel checking of continuous-time Markov chains. In Proc.the 10th International Conference on Concurrency Theory,August 1999, pp.146-162.
[26] Kindler E, Vesper T. ESTL: A temporal logic for events andstates. In Proc. the 19th International Conference of Applicationand Theory of Petri Nets, June 1998, pp.365-384.
[27] Feng L, Kwiatkowska M, Parker D. Compositional verificationof probabilistic systems using learning. In Proc. the 7thInternational Conference on Quantitative Evaluation of Systems,September 2010, pp.133-142.
[28] Bonet P, Llado C M, Puijaner R, Knottenbelt W J. PIPEv2.5: A Petri net tool for performance modelling. In Proc.the 23rd Latin American Conference on Informatics, October2007.
[29] Yuan C Y, ZhaoW, Zhang S K, Huang Y. A three-layer modelfor business processes: Process logic, case semantics and workflowmanagement. Journal of Computer Science and Technology,2007, 22(3): 410-425.
[30] Varacca D. Probability, nondeterminism and concurrency:Two denotational models for probabilistic computation
[Ph.D. Thesis]. University of Aarhus, Aarhus, Denmark,2003.
[31] Varacca D, Völzer H, Winskel G. Probabilistic event structuresand domains. Theoretical Computer Science — ConcurrencyTheory, 2006, 358(2): 173-199,
[32] Hermanns H. Interactive markov chains: The quest for quantifiedquality. In Lecture Notes in Computer Science 2428,2002, pp.57-87.
[33] Neuhäusser M R. Model checking nondeterministic and randomlytimed systems [Ph.D. Thesis]. RWTH Aachen University,Germany, 2010.
No related articles found!
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
[1] 龚振和;. On Conceptual Model Specification and Verification[J]. , 1987, 2(1): 35 -50 .
[2] 金凌紫; 朱鸿;. Systems Programming in the Functional Language FP[J]. , 1988, 3(1): 40 -55 .
[3] 刘惟一;. An Efficient Algorithm for Processing Multi-Relation Queries in Relational Databases[J]. , 1990, 5(3): 236 -240 .
[4] 徐美瑞; 刘小林;. A VLSI Algorithm for Calculating the Tree to Tree Distance[J]. , 1993, 8(1): 68 -76 .
[5] 王志坚;. Validating Inductive Hypotheses by Mode Inference[J]. , 1993, 8(2): 37 -41 .
[6] 马志方;. DKBLM——Deep Knowledge Based Learning Methodology[J]. , 1993, 8(4): 93 -98 .
[7] 马军; 马绍汉;. An O(k~2n~2) Algorithm to Find a k-Partition in a k-Connected Graph[J]. , 1994, 9(1): 86 -91 .
[8] 熊志国; 徐曦; 董士海;. CX11: A Chinese Language Supporting Interface for X Window Environment[J]. , 1995, 10(1): 15 -22 .
[9] 陈意云;. Head Boundedness of Nonterminating Rewritings[J]. , 1995, 10(3): 281 -284 .
[10] Schubert Foo; Siu Cheung Hui;. System Architectural Design for DeliveringVideo Mail over the World-Wide-Web[J]. , 1997, 12(4): 372 -385 .
版权所有 © 《计算机科学技术学报》编辑部
本系统由北京玛格泰克科技发展有限公司设计开发 技术支持：support@magtech.com.cn
总访问量：