Model-checking Data-Aware Temporal Workflow Properties with CTL-FO +
Sylvain Hall, Roger Villemaire, Omar Cherkaoui, Boubker Ghandour · 2007
Most works that extend workflow validation beyond syn- tactical checking consider constraints on the sequence of messages exchanged between services. However, these con- straints are expressed only in terms of message names and abstract away their actual data content. Using the context of the User-controlled Lightpath initiative (UCLP) hosted by the CANARIE consortium, we provide examples of real- world web service constraints where the se- quence of messages and their content are interdependent. We present CTL-FO + , an extension over Computation Tree Logic that includes first-order quantification on state vari- ables in addition to temporal operators. We show how CTL- FO + is adequate for expressing data-aware constraints, give a complete model checking algorithm for CTL-FO + and establish its complexity to be PSPACE-complete. This makes using CTL-FO + for validating workflow properties no harder than using the Linear Temporal Logic (LTL) al- ready used by some web service tools. Finally, we show how the modelling of data-aware properties is an increase in ex- pressiveness that cannot be efficiently simulated by these tools.