In this paper, we proposed a method to analyze workflows’ constraints whose templates are defined in a declarative language called DECLARE. Checking such constraints is important but known to be intractable in general. Our results show three things. First, utilizing a tree representation of workflow process called process tree, we provided necessary and sufficient conditions on the constraints. Second, those conditions enable us to not only check a given constraint in polynomial time but also find a clue for improving the net if it violates the constraint. Third, we revealed the relationship among the constraint templates.
Keywords
Petri Net, Work ow Net, DECLARE, Linear Temporal Logic (LTL), Process Tree, Con- straint
ECTI TRANSACTIONS ON COMPUTER INFORMATION TECHNOLOGY