1: \begin{abstract} 

2: The Operational Transformation (OT) approach, used in many collaborative editors, allows a group of 

3: users to concurrently update replicas of a shared object and exchange their updates in any order. 

4: The basic idea of this approach is to transform any received update operation before its execution 

5: on a replica of the object. This transformation aims to ensure the convergence of the different replicas 

6: of the object, even though the operations are executed in different orders. However, designing transformation 

7: functions for achieving convergence is a critical and challenging issue. Indeed, the transformation 

8: functions proposed in the literature are all revealed incorrect. \\

9: \par In this paper, we investigate 

10: the existence of transformation functions for a shared string altered by insert and delete operations. 

11: From the theoretical point of view, two properties -- named TP1 and TP2 -- are necessary and sufficient 

12: to ensure convergence. 

13: Using controller synthesis technique, we show that there are some transformation functions

14: which satisfy only TP1 for the basic signatures of insert and delete operations.

15: As a matter of fact, it is impossible to meet both properties TP1 and TP2 with these simple signatures.

16: 

17: %\noindent\Bd{keywords}

18: %Collaborative editors, operational transformation, proof of convergence, symbolic model checking, %controller synthesis.

19: 

20: \end{abstract}

21: