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.

This paper deals with WF-net based modeling and verification of interorganizational workflows (interworkflows for short) based on the protocol of WfMC. In the protocol, there are three patterns of interoperability: Chained, Nested, and Parallel synchronized; and an interworkflow is constructed by using those interoperability patterns. We first give a WF-net based modeling method. In this modeling method, the three interoperability patterns are respectively expressed in terms of WF-nets. They enable us to model a given interworkflow as a WF-net by connecting WF-nets representing its constituent workflows. We also indicate that if free choice WF-nets are connected by means of any combination of the three patterns then the resultant WF-net is asymmetric choice. Next we discuss verification of WF-nets obtained through the modeling method. Intuitively, a WF-net is said to be sound if, for any case, the initial state is always transformed to the final state. Unfortunately, even if every constituent WF-net is sound FC, the resultant WF-net is not always sound. We give a sufficient condition of non-soundness checkable in polynomial time. We also show that if they are connected by only the Nested pattern then the resultant WF-net is sound.