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.

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.

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.

Response property is a kind of liveness property. Response property problem is defined as follows: Given two activities α and β, whenever α is executed, is β always executed after that? In this paper, we tackled the problem in terms of Workflow Petri nets (WF-nets for short). Our results are (i) the response property problem for acyclic WF-nets is decidable, (ii) the problem is intractable for acyclic asymmetric choice (AC) WF-nets, and (iii) the problem for acyclic bridge-less well-structured WF-nets is solvable in polynomial time. We illustrated the usefulness of the procedure with an application example.

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.

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.

In this paper, we proposed reduction operators of timed Petri net for efficient model checking. Timed Petri nets are used widely for modeling and analyzing systems which include time concept. Analysis of the system can be done comprehensively with model checking, but there is a state-space explosion problem. Therefore, previous researchers proposed reduction methods and translation methods to timed automata to perform efficient model checking. However, there is no reduction method which consider observability and there is a trade-off between the amount of description and the size of state space. In this paper, first, we have defined a concept of timed behavioral inheritance. Next, we have proposed reduction operators of timed Petri nets based on timed behavioral inheritance. Then, we have applied our proposed operators to an artificial timed Petri net. Moreover, the results show that the reduction operators which consider observability can reduce the size of state space of the original timed Petri nets within the experiment.

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.

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 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.

This paper discusses formal modeling and performance evaluation for a type of dynamic change of workflow, called Migrate. Workflow means the flow of work and is designed to process similar instances, called cases. Companies need to continuously refine their current workflow in order to adapt them to various requirements. The change of a current workflow is called dynamic change of the workflow. Before changing a workflow, there exist cases in the workflow. If these cases are ignored or fall into deadlock, the changed workflow would become inconsistent. Since Ellis et al. proposed three change types, Flush, Abort, and Synthetic Cut-Over that keep consistency of workflows in 1995, various change types have been proposed, in which there is a promising change type called Migrate that is proposed by Sadiq et al. Sadiq et al. proposed the concept of Migrate, but did not give a formal model of Migrate. Meanwhile, we have proposed a measure, called change time, in order to evaluate dynamic change of workflows, and used this measure to evaluate the performance on change time for Ellis et al. 's three change types. However, the performance evaluation on change time for Migrate has not been done. In this paper, we first give a Petri-nets-based model of Migrate. Then we present a method of computing change time based on the net model. Finally, we apply the method to 270 examples and show the comparison results between Migrate and Ellis et al. 's three change types.

In this paper, we discuss a new property, named dead, of (dataflow) program nets. We say that a node of a program net is dead iff the node cannot fire once in any possible firing sequence, and furthermore the program net is partially dead. We tackle a problem of deciding whether a given program net is partially dead, named dead problem. Program nets can be classified into four subclasses: general, acyclic, SWITCH-less, and acyclic SWITCH-less nets. For each subclass, we give a method of solving dead problem and its computation complexity. Our results show that (i) acyclic SWITCH-less nets are not partially dead; (ii) for SWITCH-less nets, dead problem can be solved in polynomial time; (iii) for acyclic nets and general nets, dead problem is intractable.

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 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.

This paper deals with computation of parallel degree, PARAdeg, for (dataflow) program nets with SWITCH-nodes. Ge et al. have given the definition of PARAdeg and an algorithm of computing PARAdeg for program nets with no SWITCH-nodes. However, for program nets with SWITCH-nodes, any algorithm of computing PARAdeg has not been proposed. We first show that it is intractable to compute PARAdeg for program nets with SWITCH-nodes. To do this, we define a subclass of program nets with SWITCH-nodes, named structured program nets, and then show that the decision problem related to compute PARAdeg for acyclic structured program nets is NP-complete. Next, we give a heuristic algorithm to compute PARAdeg for acyclic structured program nets. Finally, we do experiments to evaluate our heuristic algorithm for 200 acyclic structured program nets. We can say that the heuristic algorithm is reasonable, because its accuracy is more than 96% and the computation time can be greatly reduced.

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.

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.