基于Petri网的工作流模型简化  

Reduction of Petri Net-based Workflow Model

作　　者：周从华[1] 刘志锋[1] 

机构地区：[1]江苏大学计算机科学与通信工程学院,江苏镇江212013

出　　处：《计算机科学》2008年第2期115-119,共5页Computer Science

基　　金：国家自然科学基金(No.60603041);江苏省自然科学基金(BK2006073)的资助

摘　　要：计算状态空间可达图是验证工作流正确性的主要方法,状态空间爆炸是这类方法的主要困难。文章对线性时态逻辑LTL-X描述的正确性提出了一种基于Petri网图形化简的验证方法,证明了所提出化简规则的完备性,并以实例说明了所提方法的有效性。The primary approach in verifying the workflow＇ s correctness is to compute its reachable state space. The state explosion problem is the central difficulty in such verification technique. For the correctness expressed with the linear time temporal logic LTL-X a Petri net based verification approach the employs a set of graph reduction is proposed. The completeness of the proposed method is proved. And a case study is made to demonstrate our method.

关 键 词：工作流网 PETRI网 正确性 线性时态逻辑 

分 类 号：TP393[自动化与计算机技术—计算机应用技术] TP391.41[自动化与计算机技术—计算机科学与技术]