Polynomial Time Verification of Behavioral Inheritance for Interworkflows Based on WfMC Protocol


IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E94-A   No.12   pp.2821-2829
Publication Date: 2011/12/01
Online ISSN: 1745-1337
DOI: 10.1587/transfun.E94.A.2821
Print ISSN: 0916-8508
Type of Manuscript: Special Section PAPER (Special Section on Mathematical Systems Science and its Applications)
interworkflow,  workflow net,  behavioral inheritance,  soundness,  polynomial time verification,  

Full Text: PDF(481.6KB)>>
Buy this Article

The Workflow Management Coalition, WfMC for short, has given a protocol for interorganizational workflows, interworkflows for short. In the protocol, an interworkflow is constructed by connecting two or more existing workflows; and there are three models to connect those workflows: chained, nested, and parallelsynchronized. Business continuity requires the interworkflow to preserve the behavior of the existing workflows. This requirement is called behavioral inheritance, which has three variations: protocol inheritance, projection inheritance, and life-cycle inheritance. Van der Aalst et al. have proposed workflow nets, WF-nets for short, and have shown that the behavioral inheritance problem is decidable but intractable. In this paper, we first show that all WF-nets of the chained model satisfy life-cycle inheritance, and all WF-nets of the nested model satisfy projection inheritance. Next we show that soundness is a necessary condition of projection inheritance for an acyclic extended free choice WF-net of the parallelsynchronized model. Then we prove that the necessary condition can be verified in polynomial time. Finally we show that the necessary condition is a sufficient condition if the WF-net is obtained by connecting state machine WF-nets.