International Journal of Foundations of Computer Science c ○ World Scientific Publishing Company Completeness and Realizability: Conditions for Automatic Generation of

Communicated by Editor’s name In recent years, workflow technology has greatly facilitated business process modeling and reengineering in information systems. On one hand, the separation of an application’s control structure from the implementation of its task programs simplifies and speeds up application development. On the other hand, the run-time system assists users in coordinating and scheduling tasks of a business process. As a result, the cost of doing business is reduced, and business enterprises become more responsive to new business requirements and opportunities, hence, become more competitive in the market. Several formal methods have been proposed for specifying and modeling workflows. However, most workflows are designed manually, which becomes a time-consuming and error-prone procedure when a workflow involves hundreds or thousands of task programs. A recent approach is to generate workflow automatically from a task library and a specification of the desired outcome. In this paper, we define the notions of positive and negative dependency graphs for a task library to represent the dependencies among tasks in the library. Based on these dependencies, we identified sufficient conditions for a task library to be complete, and the conditions for a workflow postcondition to be realizable from a task library. We also identified a sufficient and necessary condition for the completeness of a class of task libraries, called S-task libraries. Index terms – completeness, workflow, semantic correctness, concurrency. 1