ANALYSIS OF PETRI NETS BY STEPWISE REFINEMENTS

被引：147

作者：

VALETTE, R

机构：

[1] Laboratoire d'Automatique et d'Analyse des Systèmes, Centre National de la Recherche Scientifique, 31400 Toulouse, 7, avenue du Colonel Roche

来源：

JOURNAL OF COMPUTER AND SYSTEM SCIENCES | 1979年 / 18卷 / 01期

关键词：

D O I：

10.1016/0022-0000(79)90050-3

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

If the firing of a transition in a Petri net is considered non instantaneous, it becomes possible to replace a transition in a net P by another net P′ This allows to proceed the description and the analysis of a control structure by stepwise refinements. The necessary and sufficient conditions on P and P′ for the resulting net to be bounded and live, are given. © 1979.

引用

页码：35 / 46

页数：12

共 12 条

[1] THEORY OF ASYNCHRONOUS CONTROL NETWORKS [J].

BRUNO, J ;

ALTMAN, SM .

IEEE TRANSACTIONS ON COMPUTERS, 1971, C 20 (06) :629-&

[2]

Commoner F., 1971, Journal of Computer and System Sciences, V5, P511, DOI 10.1016/S0022-0000(71)80013-2

[3]

HACK M, 1972, THESIS MIT

[4]

HACK M, 1976, TR159 MIT LAB COMP S

[5] FORMAL VERIFICATION OF PARALLEL PROGRAMS [J].

KELLER, RM .

COMMUNICATIONS OF THE ACM, 1976, 19 (07) :371-384

[6] ANALYSIS OF STRUCTURED PROGRAMS [J].

KOSARAJU, SR .

JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1974, 9 (03) :232-255

[7]

PATIL SS, 1973, REV FR AUTOM INF FEB, P55

[8] COMPUTATION SEQUENCE SETS [J].

PETERSON, JL .

JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1976, 13 (01) :1-24

[9]

PETRI CA, 1975, INT S MATH F COMPUTE

[10]

Ramchandani C., 1973, THESIS MIT

← 1 2 →