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.

A workflow is a flow of work carried out by workers, and workflow management is to automate the flow of work. In workflow management, an actual work is carried out based on the workflow, which is called case. In order to effectively meet various requirements, it is necessary to change current workflow dynamically, which is called dynamic workflow change. When the dynamic change is required, there exist cases in the workflow. In order to handle these cases and further to keep the queuing order, the dynamic change takes period of time (called transient time) until the changed workflow becomes steady state again. During the transient time, workers are forced to do irregular work, and therefore it is important to clarify if a change type takes shorter transient time. In this paper, we do the performance evaluation on transient time of dynamic workflow changes. To do so, we first give a definition of transient time, and then propose methods of computing transient time of three change types proposed by Ellis et al. Finally, we do the performance evaluation for 90 dynamic changes by computing the transient times.

This paper deals with the performance evaluation of two types of dynamic change, called Flush and SCO (Synthetic Cut-Over), for state machine WF-nets. As an evaluation measure of dynamic change for marked graph WF-nets, change time has been used. We first generalize change time so as to apply it to dynamic change for state machine WF-nets. By using its maximum value, we evaluate the worst-case of dynamic change for state machine WF-nets. We call the maximum value as worst change time. Then under the same assumptions as our previous studies, we give methods of calculating worst change time of Flush and SCO dynamic changes. We also clarify the relation on worst change time between them. Finally we evaluate them by comparing the values of worst change time for an actual example of dynamic change.

In this paper, we discuss the parallel degree of well-structured workflow nets, WF-nets, for short. First, we give the definition of parallel degree, PARAdeg, for WF-nets. Second, we show it is intractable to compute the value of PARAdeg for acyclic well-structured WF-nets. Next we construct two heuristic algorithms to compute the value. The first algorithm is focused on nest structure and the second one is focused on the longest path. Finally, we perform an experiment to compare the two algorithms and the result is that the accuracy of the first algorithm based on nest structure was higher than that of the second one based on the longest path for most well-structured WF-nets and the accuracy of the second one is better than that of first one only when the well-structured workflow nets are mainly composed by the parallel structures.

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.

There are various existing methods translating timed Petri nets to timed automata. However, there is a trade-off between the amount of description and the size of state space. The amount of description and the size of state space affect the feasibility of modeling and analysis like model checking. In this paper, we propose a new translation method from timed Petri nets to timed automata. Our method translates from a timed Petri net to an automaton with the following features: (i) The number of location is 1; (ii) Each edge represents the firing of transition; (iii) Each state implemented as clocks and variables represents a state of the timed Petri net one-to-one correspondingly. Through these features, the amount of description is linear order and the size of state space is the same order as that of the Petri net. We applied our method to three Petri net models of signaling pathways and compared our method with existing methods from the view points of the amount of description and the size of state space. And the comparison results show that our method keeps a good balance between the amount of description and the size of state space. These results also show that our method is effective when checking properties of timed Petri 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.

The number of states is a very important matter for model checking approach in Petri net's analysis. We first gave a formal definition of state number calculation problem: For a Petri net with an initial state (marking), how many states does it have? Next we showed the problem cannot be solved in polynomial time for a popular subclass of Petri nets, known as free choice workflow nets, if P≠NP. Then we proposed a polynomial time algorithm to solve the problem by utilizing a representational bias called as process tree. We also showed effectiveness of the algorithm through an application example.

Multi-Car Elevator (MCE) systems, which consist of several independent cars built in the same shaft, are being considered as the elevators of the next generation. In this paper, we present MceSim, a simulator of MCE systems. MceSim is an open source software available to the public, and it can be used as a common testbed to evaluate different control methods related to MCE systems. MceSim was used in the group controller performance competition: CST Solution Competition 2007. This experience has proven MceSim to be a fully functional testbed for MCE systems.

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.

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.