Qualitative Analysis of WorkFlow nets using Linear Logic: Soundness Verification

被引：13

作者：

Soares Passos, Ligia Maria ^{[1
]}

Julia, Stephane ^{[1
]}

机构：

[1] Univ Fed Uberlandia, Fac Comp, BR-38400902 Uberlandia, MG, Brazil

来源：

2009 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN AND CYBERNETICS (SMC 2009), VOLS 1-9 | 2009年

关键词：

Petri net; Linear logic; WorkFlow net; Soundness; PETRI NETS;

D O I：

10.1109/ICSMC.2009.5346601

中图分类号：

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

学科分类号：

0812 ;

摘要：

This paper presents a method for the qualitative analysis of WorkFlow nets based on the proof trees of linear logic. The analysis is concerned with the proof of the correctness criterion Soundness defined for WorkFlow nets. To prove the Soundness property, a proof tree of linear logic is built for each different scenario of the WorkFlow net. Based on this approach, a method is proposed to verify in linear time if the WorkFlow net is sound.

引用

页码：2843 / 2847

页数：5

共 17 条

[1] Applying Propositional Logic to Workflow Verification [J].

Henry H. Bi ;

J. Leon Zhao .

Information Technology and Management, 2004, 5 (3-4) :293-318

[2] LINEAR LOGIC [J].

GIRARD, JY .

THEORETICAL COMPUTER SCIENCE, 1987, 50 (01) :1-102

[3]

Girault F., 1997, LOGIC PETRI NETS, V31

[4]

Gochet P., 1990, LOGIQUE METHODES INF, V1

[5] Normalized workflow net (NWF-net): Its definition and properties [J].

Li, SY ;

Song, BH .

FUTURE GENERATION COMPUTER SYSTEMS-THE INTERNATIONAL JOURNAL OF ESCIENCE, 2005, 21 (07) :1004-1014

[6]

Mantel H., 1999, TABLEAUX 99, P217

[7] PETRI NETS - PROPERTIES, ANALYSIS AND APPLICATIONS [J].

MURATA, T .

PROCEEDINGS OF THE IEEE, 1989, 77 (04) :541-580

[8]

Pradin-Chezalviel B., 1999, Proceedings 8th International Workshop on Petri Nets and Performance Models (Cat. No.PR00331), P208, DOI 10.1109/PNPM.1999.796567

[9] Reachability and temporal conflicts in t-time Petri nets [J].

Riviere, N ;

Pradin-Chezalviel, B ;

Valette, R .

9TH INTERNATIONAL WORKSHOP ON PETRI NETS AND PERFORMANCE MODELS, PROCEEDINGS, 2001, :229-238

[10]

SOARES M, 2004, P 11 IFAC S INF CONT

← 1 2 →