| [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. |