LTL model checking probabilistic Petri net system

被引：0

作者：

Liu, Yang ^{[1
,2
,3
]}

Miao, Huaikou ^{[1
,2
]}

机构：

[1] School of Computer Engineering and Science, Shanghai University

[2] Shanghai Key Laboratory of Computer Software Evaluating and Testing

[3] School of Information Science and Technology, Taishan University

来源：

International Journal of Advancements in Computing Technology | 2012年 / 4卷 / 01期

关键词：

LTL with probability; Model Checking; Probabilistic Petri net;

D O I：

10.4156/ijact.vol4.issue1.19

中图分类号：

学科分类号：

摘要：

Nonfunctional property verification is becoming more and more important to computer system. In recent decades, in order to describe not only the system function but also the system performance, researchers in the area of formal methods try to extend Petri net for modelling computer system, and the verification problem becomes the quantitative verification from the qualitative verification. In this paper, we define the reachability graph and present the solution algorithm to reachability graph; then we put forward an algorithm for linear-time temporal logic model checking probabilistic Petri net system; for demonstrating the effectiveness of this algorithm, we run an example in the modelling an verification tool which we developed.

引用

页码：172 / 178

页数：6

共 15 条

[1]

Emerson E.A., The Beginning of Model Checking: A Personal Perspective, 25 Years of Model Checking, pp. 27-45, (2008)

[2]

Clarke E., Emerson E.A., Design and synthesis of synchronization skeletons using branching time temporal logic, Proceedings of Logics of Programs: Workshop, 131, pp. 52-71, (1981)

[3]

Queille J., Sifakis J., Specification and verification of concurrent systems in CESAR, Proc. 5th Int. Symposium in Programming, 137, pp. 337-351, (1982)

[4]

Clarke E.M., The birth of model checking, 25 Years of Model Checking, pp. 1-26, (2008)

[5]

Baier C., Katoen J.-P., Principles of Model Checking, (2008)

[6]

Girault C., Valk R., Petri Nets for System Engineering: A Guide to Modeling, Verification and Application, (2003)

[7]

Albanese M., Chellappa R., Moscato V., Picariello A., Subrahmanian V.S., Turaga P., Udrea O., A constrained probabilistic petri net framework for human activity detection in video, IEEE Transactions on Multimedia, 10, 8, pp. 1429-1443, (2008)

[8]

Kudlek M., Probability in Petri Nets, Fundamenta Informaticae, 67, pp. 121-130, (2005)

[9]

Varacca D., Nielsen M., Probabilistic petri nets and Mazurkiewicz equivalence, (2003)

[10]

Liu Y., Miao H., Zeng H., Li Z., Probabilistic Petri Net and Its Logical Semantics, Proceedings of 9th ACIS International Conference on Software Engineering Research, Management and Applications(SERA 2011), pp. 73-78, (2011)

← 1 2 →