[Inductive Step :] **We assume that the spuriousness of a conflict reported for the queries with**
ontological conflict in n **steps are true. We now prove that the spuriousness of a conflict that is reported**
in (n + 1) steps are correct. Consider the VerifyConflict **function call at Algo. 3 and without loss of**
generality, we can assume this function call as the (n + 1)th **function call (in the order of returning**
of the function calls). Therefore the other calls are recursive calls done by the VerifyConflict **to itself.** The following two cases are possible.

a. The conflict may be detected as spurious by some call which is not the (n + 1)th **call. In this case**
the spuriousness of the conflict is correct by the inductive hypothesis.

b. The conflict is detected as spurious at the (n + 1)th call to VerifyConflict**. All other previous**
calls to VerifyConflict add a table to Ht **and the set of tables are kept in** S
t**. After that, function**
GenerateAssignableSet is called to compute the assignable set for the set of previously instantiated variables v in the query q **with ontological conflict. It follows from the description of the function,**
that this function restricts the set of valuations of v **by taking the natural join with the valuations** of variables in RestrictSet(v**). Since the conflict is not detected as spurious in the variables in**
RestrictSet(v), when the function detects the conflict as spurious, the statement δ == ∅ **is true.**
Therefore in the protocol q **is not reachable from the start state of the protocol.** ⊓⊔
Theorem 4. **[Completeness] If there is a spurious conflict on the set of variables** v
′
**, where** v
′ = v ∪
RestrictSet(v) and v is the previously instantiated variable set specified in a query q of protocol P **with**
ontological conflict, the algorithm reports it. We do the proof by establishing the contrapositive of the statement, i.e. Algorithm 3 reports the ontological as not spurious, if q **is reachable from the start state**
of P.

Proof. **Suppose** v
′ = {ϕ1, ..., ϕn}**. Let the valuations of the variables in** v
′ are (val1, ..., valn**) when**
the conflict in q **is not spurious. In this case the conflict may occur in the following way. Consider**
the VerifyConflict **function calls made to determine the spuriousness of the ontological conflict in** q, among which the first call is done by Algo. 3 and the subsequent calls are recursive calls. The conflict is detected as not spurious, only if all the recursive calls to VerifyConflict add a table to Ht **and the**
set of tables are kept in S
t. Since the conflict is determined as not spurious, the statement δ **is not**
empty. Therefore in P, q **is reachable from the start state of the protocol using any instantiation of**
variables belonging to δ. ⊓⊔

## 6 Related Works

Different aspects of web service interaction have been an active area of research. However most of these researches consider the interaction at syntactic level. Foster et. al. **addressed the compatibility**
verification of web services in [11]. They adopted a model based approach for checking the compatibility of web services at different level of abstraction. However the **semantics of exchanged data is**
not addressed by the researchers. In [12] researchers address the interaction among web services which is asynchronous in nature and propose a design pattern to help the **development of composite web** services based on asynchronous interaction. Zhao et. al. **provides a formal treatment of web service**
choreography in [13]. They define a formal model of the of WS-CDL and propose a methodology to formally verify the correctness of a choreography using the model checker SPIN. In [14] authors proposed a formalism for specifying the web service interfaces. They discuss **about three kind of constraints** which can be put by a web service interface. The propositional constraints **are imposed by an interface**
by specifying the methods that can be invoked by the clients along with the constraints on the input and output parameters(signature constraints). Protocol Constraints **specify the temporal requirements** on the sequence of the method invocations. An algorithm is proposed to check compatibility among 41