Formalizing Workflow with Location Constraints by Colored Petri Nets

Workflow provides a promising solution for organizations to achieve their business goals by collaborations between users. With the assistant of mobile and handheld devices, users may perform workflow tasks in different locations. Hence, some location-based restrictions can be defined on these tasks and users according to the enterprise business rules. In this paper, we propose a method to model workflow with location constraints based on colored Petri Nets(CPN). The location constraints are defined as predicate logic expressions. Then all these logic expressions are combined with the CPN workflow model. After formalization, the CPN analysis methods and tools can be used to analyze the correctness of the workflow and the constraints.