Automatic DAG-Based Service Composition: A Model Checking Approach

We propose a novel approach based on model checking for automated non-linear service composition. Modeling services as interleaved processes, we formulate the service composition problem as verifying a safety property and show that multiple non-linear compositions can be constructed from the counter-example. The state explosion problem is tackled by using service clustering and computing service closures.