PROVING TEMPORAL PROPERTIES OF PETRI NETS

被引：0

作者：

BRADFIELD, JC

机构：

来源：

LECTURE NOTES IN COMPUTER SCIENCE | 1991年 / 524卷

关键词：

PETRI NETS; TEMPORAL LOGIC; TABLEAU SYSTEMS; MODEL-CHECKING;

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We present a sound and complete tableau system for proving temporal properties of Petri nets, expressed in a propositional modal mucalculus which subsumes many other temporal logics. The system separates the checking of fix-points from the rest of the logic, which allows the use of powerful reasoning, perhaps specific to a class of nets or an individual net, to prove liveness and fairness properties. Examples are given to illustrate the use of the system. The proofs of soundness and completeness are given in detail.

引用

页码：29 / 47

页数：19

共 50 条

[31] An introduction to Petri nets
Barad, M
INTERNATIONAL JOURNAL OF GENERAL SYSTEMS, 2003, 32 (06) : 565 - 582
[32] Statechartable Petri nets
Eshuis, Rik
FORMAL ASPECTS OF COMPUTING, 2013, 25 (05) : 659 - 681
[33] On hybrid Petri nets
David, R
Alla, H
DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2001, 11 (1-2): : 9 - 40
[34] The concepts of Petri nets
Desel, Joerg
Reisig, Wolfgang
SOFTWARE AND SYSTEMS MODELING, 2015, 14 (02) : 669 - 683
[35] Possibilistic Petri nets
Cardoso, J
Valette, R
Dubois, D
IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART B-CYBERNETICS, 1999, 29 (05): : 573 - 582
[36] On Hybrid Petri Nets
René David
Hassane Alla
Discrete Event Dynamic Systems, 2001, 11 : 9 - 40
[37] Diagnosability of Petri nets
Wen, YL
Jeng, MD
2004 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN & CYBERNETICS, VOLS 1-7, 2004, : 4891 - 4896
[38] Clustering for Petri nets
Keller, W
THEORETICAL COMPUTER SCIENCE, 2003, 308 (1-3) : 145 - 197
[39] Lending Petri nets
Bartoletti, Massimo
Cimoli, Tiziana
Pinna, G. Michele
SCIENCE OF COMPUTER PROGRAMMING, 2015, 112 : 75 - 101
[40] The concepts of Petri nets
Jörg Desel
Wolfgang Reisig
Software & Systems Modeling, 2015, 14 : 669 - 683

← 1 2 3 4 5 →