Logic based modeling and analysis of workflows

We propose Concurrent Transaction Logic (CTR) as the language for specifying, analyzing, and scheduling of workflows. We show that both local and global properties of workflows can be naturally represented as CTR formulas and reasoning can be done with the use of the proof theory and the semantics of this logic. We describe a transformation that leads to an efficient algorithm for scheduling workflows in the presence of global temporal constraints, which leads to decision procedures for dealing with several safety related properties such as whether every valid execution of the workflow satisfies a particular property or whether a workflow execution is consistent with some given global constraints on the ordering of events in a workflow. We also provide tight complexity results on the running times of these algorithms.