Abstract: According to the concurrent workflow patterns, split and anyorder, and their implementation in the systems adopting the central architecture, the interval temporal logic is extended by two new operators: shuffle and restricted shuffle. The formulas connected with the new operators are suitable for representing concurrent workflows, which is proved with the partial-order relationship among the states maintained by the workflow and the length relationship among the intervals that satisfy those formulas describing the workflow and the participating activities. An example is given to illustrate how to use the extended interval temporal logic to represent the activities and the concurrent workflow composed of these activities. The interval temporal logic model for concurrent workflows can be obtained by this method. This model can be employed to verify the liveness and safety of concurrent workflows by utilizing some tools and theories based on interval temporal logic, which guarantees the reliability of the design of concurrent workflows.

Key words: concurrent workflow, interval temporal logic, deterministic finite automata