Workflow nets (WF-nets for short) are a subclass of Petri nets and are used for modeling and analysis of workflows. Soundness is a criterion of logical correctness defined for WF-nets. A WF-net is said to be sound if it satisfies three conditions: (i) option to complete, (ii) proper completion, and (iii) no dead tasks. In this paper, focusing our analysis on acyclic free choice WF-nets, we revealed that (1) Conditions (i) and (ii) of soundness are respectively equivalent to the liveness and the boundedness of its short-circuited net; (2) The decision problem for each condition of soundness is co-NP-complete; and (3) If the short-circuited net has no disjoint paths from a transition to a place (or no disjoint paths from a place to a transition), each condition can be checked in polynomial time.

Workflow nets (WF-nets for short) are a standard way to automate business processes. Well-Structured WF-nets (WS WF-nets for short) are an important subclass of WF-nets because they have a well-balanced capability to expression power and analysis power. In this paper, we revealed structural and behavioral properties of WS WF-nets. Our results on structural properties are: (i) There is no EFC but non-FC WF-net in WS WF-nets; (ii) A WS WF-net is sound iff it is a van Hee et al.'s ST-net. Our results on behavioral properties are: (i) Any WS WF-net is safe; (ii) Any WS WF-net is separable; (iii) A necessary and sufficient condition on reachability of sound WS WF-net (N,[pIk]). Finally we illustrated the usefulness of the proposed properties with an application example of analyzing workflow evolution.

An organization may have two or more similar workflows as a result of workflow evolutions or mergers and acquisitions. We should grasp the common behavior of those workflows to consolidate the management of them and/or to do business process reengineering. Workflows can be modeled as a particular class of Petri nets, called workflow nets. The common behavior of two or more workflow nets can be represented as a superclass under the behavioral inheritance of those workflow nets. In this paper, we tackled a problem of extracting a superclass from two workflow nets, named Superclass Extraction problem. We first gave a definition of the problem. Next we proposed a procedure to solve the problem on the basis of process mining technique. Then we gave an application of the proposed procedure.

Many actual systems, e.g. computer programs, can be modeled as a subclass of Petri nets, called bridge-less workflow nets. For bridge-less workflow nets, we revealed the following properties: (i) any acyclic bridge-less workflow net is free choice; (ii) an acyclic bridge-less workflow net is sound iff it is well-structured; and (iii) any sound bridge-less workflow net is well-structured. We also proposed a necessary and sufficient condition to decide whether a given workflow net is bridge-less, and then constructed a polynomial-time procedure for it.

Workflow nets (WF-nets for short) are a mathematical model of real world workflows. A WF-net is often updated in accordance with the change of real world. This may cause places that are redundant from the viewpoint of the behavior. Such places are called implicit. We first proposed a necessary and sufficient condition to find implicit places. Then we proved that removing of implicit places is a reduction operation which forms branching bisimilarity. We also constructed an algorithm for the reduction. Next, we applied the proposed reduction operation to WF-net refactoring. Then we showed the usefulness of the proposed refactoring with two examples.

A workflow net (WF-net for short) is a Petri net which represents a workflow. There are two important subclasses of WF-nets: extended free choice (EFC for short) and well-structured (WS for short). It is known that most actual workflows can be modeled as EFC WF-nets; and acyclic WS is a subclass of acyclic EFC but has more analysis methods. A sound acyclic EFC WF-net may be transformed to an acyclic WS WF-net without changing the observable behavior of the net. Such a transformation is called refactoring. In this paper, we tackled a problem, named acyclic EFC WF-net refactorizability problem, that decides whether a given sound acyclic EFC WF-net is refactorable to an acyclic WS WF-net. We gave two sufficient conditions on the problem, and constructed refactoring procedures based on the conditions. Furthermore, we applied the procedures to a sample workflow, and confirmed usefulness of the procedures for the enhancement of the readability and the analysis power of acyclic EFC WF-nets.

A workflow may be extended to adapt to market growth, legal reform, and so on. The extended workflow must be logically correct, and inherit the behavior of the existing workflow. Even if the extended workflow inherits the behavior, it may be not logically correct. Can we modify it so that it satisfies not only behavioral inheritance but also logical correctness? This is named behavioral inheritance preserving soundizability problem. There are two kinds of behavioral inheritance: protocol inheritance and projection inheritance. In this paper, we tackled protocol inheritance preserving soundizability problem using a subclass of Petri nets called workflow nets. Limiting our analysis to acyclic free choice workflow nets, we formalized the problem. And we gave a necessary and sufficient condition on the problem, which is the existence of a key structure of free choice workflow nets called TP-handle. Based on this condition, we also constructed a polynomial time procedure to solve the problem.

Workflow nets are a standard way for modeling and analyzing workflows. There are two aspects in a workflow: definition and instance. In form of workflow nets, a workflow definition and a workflow instance are respectively represented as a net structure and a marking. The correctness of the workflow definition can be checked by using a workflow nets' property, called soundness. On the other hand, the correctness of the workflow instance can be checked by using a Petri nets' well-known property, called reachability. The reachability problem is known to be intractable. In this paper, we have shown that the reachability problem for (i) sound extended free-choice workflow nets with a marking representing one workflow instance or (ii) acyclic well-structured workflow nets with a marking representing one or more workflow instances can be solved in polynomial time.

A workflow net N may be extended as another workflow net N' by adding nodes and arcs. N' is intuitively called a subclass of N under protocol inheritance if we cannot distinguish those behaviors when removing the added transitions. Protocol inheritance problem is to decide whether N' is a subclass of N under protocol inheritance. It is known that the problem is decidable but is intractable. Even if N is a subnet of N', N' is not always a subclass of N under protocol inheritance. In this paper, limiting our analysis to protocol inheritance between acyclic extended free-choice workflow nets and their subnets, we gave a necessary and sufficient condition on the problem. Based on the condition, we also constructed a polynomial time procedure for solving the problem.

A workflow net (WF-net for short) is a Petri net which represents a workflow. There are two important subclasses of WF-nets: extended free-choice (EFC for short) and well-structured (WS for short). It is known that most actual workflows can be modeled as EFC WF-nets; Acyclic WS is a subclass of acyclic EFC but has more analysis methods. An acyclic EFC WF-net may be transformed to an acyclic WS WF-net without changing the external behavior of the net. We name such a transformation Acyclic EFC WF-net refactoring. We give a formal definition of acyclic EFC WF-net refactoring problem. We also give a necessary condition and a sufficient condition for solving the problem. Those conditions can be checked in polynomial time. These result in the enhancement of the analysis power of acyclic EFC WF-nets.

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.

Workflow nets (WF-nets) are Petri nets which represent workflows. Soundness is a criterion of logical correctness defined for WF-nets. It is known that soundness verification is intractable. In this paper, we propose a method to verify soundness using a Linear Temporal Logic (LTL) model checking tool, SPIN. We give an LTL necessary and sufficient condition to verify soundness for WF-nets without livelock. Acyclic WF-nets have no livelock, but cyclic WF-nets may have livelock. We also give a necessary and sufficient condition to verify livelock. Meanwhile, we show that any LTL model checking tool cannot verify soundness for WF-nets with livelock. We give necessary conditions to verify soundness for them. Those conditions enable us to use SPIN even if a given WF-net has livelock. We also develop a tool to verify soundness based on our method. We show effectiveness of our method by comparing our tool with existing soundness verification tools on verification time for 200 cyclic ACWF-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.

This paper proposes a new change type for dynamic change of workflows, named Selective Shift. Workflow technology is being introduced in many companies. Workflows are business processes that allow for computerized support. The goal of workflow technology is to process workflow instances, called cases, as efficiently as possible. Companies need to change their workflows in order to adapt them to various requirements. Dynamic change is to change workflows having running cases. The most important issue in dynamic change is how running cases should be handled. Ellis et al. and Sadiq et al. have proposed change types that prescribe how to handle running cases. Their change types handle running cases collectively. If a change type can handle running cases separately, the change type would be more flexible and efficient than the conventional change types. However, there is no any change type that can handle running cases separately. Selective Shift to be proposed can handle running cases separately. We first present the concept and definition of Selective Shift. Then we give a method to handle running cases separately. Furthermore we give methods to handle running cases so that dynamic change becomes most efficient on one evaluation measure, called change time. Finally we compare Selective Shift with the conventional change types on change time by using 270 examples of dynamic change.

This paper proposes methods of computing maximum throughput for Petri nets that model workflows including resources, called WF-nets with resources. We first propose the formal definitions of WF-nets with resources and their subclasses: marked graph/state machine WF-nets with conflict-free resources (CF-Res-MG/SMWF-nets). We also show several properties of CF-Res-MG/SMWF-nets. Next we give the methods of computing maximum throughput for CF-Res-MG/SMWF-nets under condition that all tokens have to be processed in the order of First-In First-Out (FIFO). Concretely, for CF-Res-MGWF-nets, on the basis of Ramamoorthy's method of computing cycle time, we give an algorithm of computing maximum throughput under the FIFO condition. For CF-Res-SMWF-nets, there is not any method of computing maximum throughput under the FIFO condition. So we are the first to give an algorithm of computing maximum throughput for CF-Res-SMWF-nets under the FIFO condition. Finally we show an example of computing maximum throughput by using our method.

A workflow is a flow of work carried out in parallel and in series by people. In order to improve efficiency, it is required to change the current workflow dynamically. Since dynamic change of workflows may probably make the series of work inconsistent, it is necessary to find out consistent change of workflow. As consistent ways, three types of dynamic changes: flush, abort, and synthetic cut-over (SCO), have been proposed. However, the concrete analysis and evaluation have not been done. To do the performance evaluation for the dynamic workflow changes, comparison of the times (called change time) cost in the individual change and the methods how to obtain such times become ever important. In this paper, we first give a definition of change time and then propose the computation methods individually for each change type. Finally, we do experiments to evaluate the performance of three changes by doing the comparison of the change times.