Referee: 1 The paper has a simple aim: to define a translation of pure MAs into pi-calculus that preserves and (somehow) reflects the operational semantics. 

The encoding show how the two paradigms (ambients vs name passing) can be related. This is indeed an interesting topic, yet the reasons for the validity of such a study could be better argued with some references to the literature. To sum it up just in the opening phrase of the article, "The comparison of different languages is a crucial topic in the area of formal languages”, is definitively insufficient.  ================================================================================================================================================================ R. The opening phrase has been reformulated: “The comparison of different languages is a crucial topic in the area of formal languages, see for example~\cite{S96,P03,BGZ09}, is a tool to characterise the expressiveness power of different languages, whereas all the languages have the same computational power. This kind of investigation plays an important role in modelling case studies which come from different areas and at different abstract levels.” [S96] Sangiorgi, D. (1996) pi-Calculus, Internal Mobility, and Agent-Passing Calculi. Theoretical Computer Science 167 (1&2), 235–274. Elsevier. [P03] Palamidessi, C. (2003) Comparing the expressive power of the synchronous and the asynchronous pi-calculus. Mathematical Structures in Computer Science 15 (5), 685–719. Cambridge University Press. [BGZ09] Busi, N. and Gabbrielli, M. and Zavattaro, G. (2009) On the expressive power of recursion, replication and iteration in process calculi. Mathematical Structures in Computer Science 19 (6), 1191–1222. Cambridge University Press. =============================================================================================================================================================================== The author remarks that the two paradigms "have different expressive power", and indeed the title of the paper ("On the expressiveness of the pi-calculus and the Mobile Ambients”) seems to underline that relative expressiveness is a main issue of the paper. To a certain extent, this is misleading, since the encoding in itself does not explicitly address the issue, which is not further elaborated. I would then choose a title that better adheres to the scope of the paper, meaning, a sound and complete encoding of MAs into pi-calculus. 
================================================================================================================================================================ R. Yes, it is true, anyway I think that due to the divergence introduced by our translation the title “ a sound and complete encoding of MA into pi-calculus” could raise controversy. Thus, the title has been changed as the following: On the expressiveness of $\pi$-calculus for encoding Mobile Ambients. ================================================================================================================================================================ 
The section of fairness makes for an hard read. Without any example, it is almost impossible to understand. Please make clear how the definition of the new labels is related to strong fairness, and indeed how it helps to avoid loops. A carefully crafted example may suffice, without making the section more formal, and dropping the logical trappings altogether. As it stands, the section does not add to the paper. =============================================================================================================================================================================== R. The section of fairness has been removed. We have added the section '4.2 Run time supports to avoid loops' where we introduce two run time methods to avoid loops. =============================================================================================================================================================================== 

 Some detailed comments, including typos and some specific remarks on the structure of the article, can be found in the annotated .pdf.  
=============================================================================================================================================================================== R. All these corrections have been made. =============================================================================================================================================================================== 
Summing up, I would the suggest acceptance with a revision taking into account the issues of drawing a more careful set of motivations and of restructuring the fairness section.  -------- Referee: 2 Mobile Ambients (MA) was proposed about 13 years ago by Cardelli and Gordon, and it is considered by many the second most prominent mobile process calculus, the first one being the \pi calculus (\pi). 

This paper shows an encoding of MA into \pi and proves its correctness and completeness in terms of operational correspondence. 

There have been several encodings of \pi into MA, but, to my knowledge, only one going in the other direction (i.e., from MA to \pi). This latter one, by Ciobanu et al, however, introduced a central coordination process (a process acting as a central capability execution controller), while the encoding presented in this paper does not require such a process.  The lack of a coordination process is an important feature, that characterizes a "good" encoding and testifies the expressiveness of the target language.  This is certainly very interesting, since it was not clear (at least not to this reviewer), up to now, that \pi is expressive enough to capture all the complicated mechanisms of MA. Furthermore, as argued in the paper, it is useful as it allows reusing for MA some of the tools that have been developed for \pi. (Actually the paper says "all the tools". This I don't believe: for some tools like those based on bisimulation, one would need a tighter relation than operational correspondence.) 

The encoding presented in the paper is ingenious and technically very involved. I believe that the complication is intrinsic, i.e. the mechanisms of MA are quite cryptic and when you try to mimic them with the more elementary mechanisms of \pi, all the intricacy comes to surface. 

I cannot say I understood all the details of the encoding, but I think I got the "spirit", and I am convinced that it works.  --- Comments for the authors: 

- The paper is reasonably well written, except for the English that in some points is not very fluid. 
  - You claim that your encoding is compositional, but technically it is not: the encoding, T, first generates an Amb(Top) process, and then it applies an other function, T_s, to the source process. T_s is compositional, but T is not.  ================================================================================================================================================================ R. I added in the paper some more details to show the compositionality of the encoding (I report these additional details here below). “It is easy to show that our encoding is compositional with respect to the parallel and the non-deterministic operators, up to preliminarily settings. In fact, if we have Q_1 = {\cal T}(P_1), Q_2 = {\cal T}(P_2), and Q_3 = {\cal T}(P_1|P_2), where Q_1 = (\nu \tilde{n}) (Amb(top)| {\cal T}_a(P_1,top)), Q_2 = (\nu \tilde{m}) (Amb(top)| {\cal T}_a(P_2,top)), and Q_3 = (\nu \tilde{\omega}) (Amb(top)| {\cal T}_a(P_1|P_2,top)) we can obtain the direct encoding of P_1|P_2 by setting {\cal T}(P_1|P_2) = (\nu \tilde{z}) Amb(top)|{\cal T}_a(P_1,top) | {\cal T}_a(P_2,top), where \tilde{z} = \tilde{n} \cup \tilde{m} =\tilde{w}. It is important to remark that no \alpha-renaming is applied on the name sets \tilde{n}, and \tilde{m} in building the set \tilde{z}.” =============================================================================================================================================================================== - Related to previous point: The encoding of the parallel operator is not homomorphic (although T_s is). Homomorphism in the translation of the parallel operator was one of the conditions required by Palamidessi   for the encoding to be "reasonable" (cfr. her papers on the separation between the asynchronous and the full pi-calculus, MSCS 2003). This condition fully justify the claim that the encoding preserves the degree of distribution.  Since your encoding is not homomorphic, you should justify that you are not introducing a coordinator process (i.e., that Amb(Top) does not act as such a coordinator process), otherwise you cannot claim that your encoding is substantially better than the one by Ciobanu et al. Please discuss in detail the role of Top(Amb) in the encoding.  =============================================================================================================================================================================== R. I added some more details to show the compositionality of the encoding, as reported in the following. “It is important to remark that our encoding does not rely on a process acting as a central capability execution controller, in particular the process Amb(top) only acts as the encoding of the topmost parent ambient, that has not a syntactical correspondence in the MA processes, for the encoding of top level ambients. In fact, our encoding is based on a network of channels where each encoding of an ambient knows its unique name and the unique name of the encoding of its parent ambient. For the top level ambients in the MA processes there is not such parent ambient, and we force the encoding function to add this further process Amb(top): T (P) = (ν \tilde{n})(Amb(top)|Ta (P)). The behaviour of the process Amb(top) can be checked in Table 14 in the Appendix, and it is possible to verify that it is a short version of the code of Amb(. . . ) processes, as Amb(top) can not be the target of a capability (on channels intop, outtop, and opentop) and hence it is not equipped to act as the target ambient of a capability.” =============================================================================================================================================================================== - Your encoding introduces divergence. Preservation of termination was the other condition required by Palamidessi in her MSCS 2003 paper. Without that condition, you could for example try again and again  pick up two arbitrary processes until you find the right ones whose capabilities match. If I understand correctly, your encoding does not do this, and the divergence you introduce is a "good divergence" that could be ruled out by a fairness  rule (cfr. Page 21). Unfortunately this section is not very clear.    Please give an intuition of what this fairness condition means, and  justify better that your encoding does not introduce bad forms of divergence. ===============================================================================================================================================================================   R. The section of fairness has been removed. We have added the section '4.2 Run time supports to avoid loops' where we introduce two run time methods to avoid loops. ===============================================================================================================================================================================
 -------- Referee: 3 Review for On the expressiveness of the pi-calculus and Mobile Ambients submitted by Linda Brodo to Mathematical Structures in Computer Science ================ The paper presents an encoding of Cardelli and Gordon's Mobile Ambients (MA) into the (mixed choice, match and mismatch) pi-calculus. It starts presenting the two calculi, then the translation and some of its properties, together with proofs. It also compares the result with the literature on the subject. I have several general critiques to this work: 1. is this work aimed at showing the power of PI in modeling MA? I wouldn't say so, because the encoding introduces divergence. It is now a well established feature in the community that an encoding, to be reasonable, cannot introduce divergence. Works by Palamidessi, Nestmann, Carbone, Gorla and many others have contributed to establishing this principle. For example, if we admit divergence, mixed choice pi can be encoded into asynchronous pi (Nestmann 2000), whereas it is now well-established that mixed choice pi has an expressive power that cannot be rendered in asynchronous pi. Several other recent works in the concurrency community (e.g., by Van Glabbeek, Sangiorgi, ...) now rely on this principle. But also outside from the concurrency community, this principle has many supporters. Take, for example, the distributed computing community, where long ago Maurice Herlihy (TOPLAS'91) discussed the impossibility of encoding different synchronization primitives. All those results rely on the fact that the encoding can't introduce divergence. Without this assumption, all the results proved therein would vanish. Moreover, the discussion on fairness at page 21 is not convincing: the very same assumption would save, e.g., Nestmann's divergent encoding of mixed choice in asynchronous pi. ============================================================================================================================= R. We are aware that our encoding can have diverging traces, and that it can not be classified as a classical encoding, due to the many above mentioned results that have settled the principle that "an encoding cannot introduce divergence". Our work defines an encoding "as precise as possible" with the aim of showing the double role of an ambient: giving an identity to processes and identifying a location. However, in our encoding the divergence is due to loops of limited length returning in the starting state. We have added the new section 'Run time supports to avoid loops' where we give two techniques to avoid loops to be implemented at execution time. Thus, our divergence is harmless from a practical point of view. ============================================================================================================================= 2. is this work aimed at showing how the nested structure of MA can be rendered into the "plain" structure of pi? Maybe yes, but as said before, the rendering is not satisfactory because of divergence. Moreover, the way in which the paper is written and in which the encoding is explained are neither satisfactory. At page 8, there is an informal explanation, but then there are 4 pages full of pi-processes (considering both the text and the appendix) that are almost not explained at all. Moreover, the extreme complexity of the encoding makes it very hard to follow and can be hardly considered for a concrete implementation of MA into some programming language, also because of the introduction of divergence, previously discussed. ============================================================================================================================= R. We have already discussed the divergence problem; to help intuition, we have added Example 2 where we have detailed a complete execution of a simulating trace equipped with a series of graphics showing the use of private channels for the communications between the processes involved in a simulating trace. We have also added Figure 1 to give a graphical representation of the relationship between the MA LTS and the pi-calculus LTS, including aborting traces (responsible of the introduction of the divergence). ============================================================================================================================= Furthermore, an encoding of MA in PI has already been done several years ago by Ciobanu. The critique moved by the author to Ciobanu's work is that it introduces a central coordinating process; also the present encoding has such a process (Amb(top) in Def.3). ============================================================================================================================= R. The process Amb(top) plays no any kind of central coordinating control. It has been added to complete the encoding of the hierarchical ambient structure. Roughly, in the encoding processes, the original topmost MA ambients need a parent ambient. Thus, the only role that the process Amb(top) plays is to be the topmost parent and only interacts on channel name "top". Moreover it has limited functionalities with respect to the other processes of type Amb(...), as it can not be the target of any capability simulation. In the paper we added the following explanation: It is important to remark that our encoding does not rely on a process acting as a central capability execution controller, in particular the process Amb(top) only acts as the encoding of the topmost "parent ambient", that has not a syntactical correspondence in the MA processes, for the encoding of top level ambients. In fact, our encoding is based on a network of channels where each encoding of an ambient knows its unique name and the unique name of the encoding of its parent ambient. For the top level ambients in the MA processes there is not such "parent" ambient, and we force the encoding to add this further process Amb(top): {\cal T}(P) = (\nu \, \tilde{n}) (Amb(top)|{\cal T}_a(P)). The behaviour of the process Amb(top) can be checked in Table[14] in the Appendix, and it is possible to verify that it is a short version of the code of Amb(\dots) processes, as Amb(top) can not be the target of a capability (on channels intop, outtop, and opentop) and hence it is not equipped to act as the target ambient of a capability. ============================================================================================================================= Of course, the role played by such a process in Ciobanu's work is much more critical, but still the present encoding is not compositional w.r.t. parallel composition. At page 2, the author says that compositionality can be proved, but I can't find any proof (actually, this should not be something that needs a proof; it should be immediate from the definition of the encoding). Maybe, you can prove that [P|P] behaves like (w.r.t. some form of equivalence) [P] | [P], but this doesn't mean that the encoding is compositional! ============================================================================================================================= R. Concerning this point, in the article we have added the following explanation: It is easy to show that our encoding is compositional with respect to the parallel and the non-deterministic operators, up to preliminarily settings. In fact, if we have Q_1 = {\cal T}(P_1), Q_2 = {\cal T}(P_2), and Q_3 = {\cal T}(P_1|P_2), where Q_1 = (\nu \tilde{n}) (Amb(top)| {\cal T}_a(P_1,top)), Q_2 = (\nu \tilde{m}) (Amb(top)| {\cal T}_a(P_2,top)), and Q_3 = (\nu \tilde{\omega}) (Amb(top)| {\cal T}_a(P_1|P_2,top)) we can obtain the direct encoding of P_1|P_2 by setting {\cal T}(P_1|P_2) = (\nu \tilde{z}) Amb(top)|{\cal T}_a(P_1,top) | {\cal T}_a(P_2,top), where \tilde{z} = \tilde{n} \cup \tilde{m} =\tilde{w}. It is important to remark that no \alpha-renaming is applied on the name sets \tilde{n}, and \tilde{m} in building the set \tilde{z}. ============================================================================================================================= 3. the encoding works well only for pure MA, i.e. MA without name passing. It is well- known that such a fragment is Turing complete, but the introduction of name passing is something very useful in practice. It has the same impact of passing from CCS to PI... I'm not saying that a "good" encoding of pure MA into PI would not be interesting; I just complain about the fact that the encoding cannot be scaled to encompass this important feature. ============================================================================================================================= R. We did not consider name passing. However, we are confident that we could encode name passing with the main limitation that input variables can not be used for giving names to ambients. For example we could not allow the following use of input variables: a(x).b(y).x[in y]. ============================================================================================================================= 4. Last but not least, I honestly find the subject of the work quite old-fashion: nobody is working on ambients anymore (actually, already for the last 5/6 years at least). Thus, I have serious concerns on the interest of this work and on the impact it may have on the community whenever it will appear in the journal. ============================================================================================================================= R. It is true that the subject of the work is not new. Anyway, the exploration of this topic allowed us to go deep through the nature of the synchronization mechanism of mobile ambients: we encode a MA ambient as a pi-calculus process. From this study we have introduced a new multiparty calculus [1] that allows us to use the same modeling technique: modeling locations as processes, also in the biological field [2]. Further studies could involve the modeling of features such as locations and shapes (that seem to be important biological features) as processes. [1] Bodei, C. and Brodo, L. and Bruni, R. (2013) Open Multiparty Interaction. In N. Marti-Oliet and M. Palomino (editors) Recent Trends in Algebraic Development Techniques, 2013, Lecture Notes in Computer Science 7841, 1–23. Springer Berlin Heidelberg. [2] Bodei, C. and Brodo, L. and Bruni, R. (2014) A Flat Process Calculus for Nested Membrane Interactions. Scientific Annals of Computer Science 24(1), 91--136. 'A.I. Cuza' University Press, Iacsi. ============================================================================================================================= Among the above critiques, the first and the last ones are really fundamental and undermine all the work; the second one can partly be remedied by a severe rework of the presentation of the paper; the third one is minor, but still has an impact. To sum up, I really fail to see a motivation for this work. Usually, an encoding of A into B is either given to show the power of B or to provide an implementation of A (provided that B has one). However, for the reasons given above, the encoding presented cannot be considered as a way for showing the power of PI (critique 1) and cannot either be considered a reasonable implementation of MA into PI (critique 1 and 2). The only suggestion that comes to my mind is to see whether a simpler fragment of the calculus (e.g., the one without open - that is still Turing complete, see the work by Maffeis in TCS 2005) can give rise to a non-diverging (and, maybe, scalable to name passing) encoding. Then, the author can informally discuss how the open capability can be rendered, why this introduces divergence and if a non-diverging encoding is possible at all. ============================================================================================================================= R. The encoding technique we have applied would still introduce divergence even considering this simpler fragment of MA. However, we have defined a technique for making the divergence harmless as we report in the last section of the paper. ============================================================================================================================= To conclude, I don't suggest acceptance of this work and I don't either consider a second round of revision worthwhile (unless the paper is radically changed, at least to get rid of divergence). For this reason, I've not gone through the proofs because I don't consider this paper worth of publication, even if all proofs were correct. By now, I think that a technical report that completes the conference version of this work is enough. MINOR COMMENTS what you call "soundness and completeness" are called "operational correspondence" or "operational soundness and completeness"; you should use the current terminology. ============================================================================================================================= OK. Done. ============================================================================================================================= why do you give the semantics for MA in a reduction style and the one for pi as an LTS? ============================================================================================================================= R. They are the classical version of semantics for the two calculi and we had no problem to use them. ============================================================================================================================= beginning of sect. 4.1.: it is totally obscure to me what is the problem you're facing here and how the introduction of brackets solves it. ============================================================================================================================= R. In the paragraph preceding Subsection 4.1 we have added the following explanation: The problem is that when P -> P' by executing an open capability, its pi-calculus encoding T(P) can simulate the execution of the previous open capability, T(P) ->* Q', but Q' contains an Opened(...) process that have no syntactical correspondence in P', and hence we have that T(P) \noequiv Q'. ============================================================================================================================= Example 1: process P can only execute one of the two open capabilities (the top level one)... Moreover, in the graphical representation, in the OUT and in the bottom OPEN node, I think that outa and openb should be outn and openn. ============================================================================================================================= OK. Done. ============================================================================================================================= Finally, always for those two nodes, I cannot understand the meaning of the edges labeled with "top" ============================================================================================================================= R. "top" is the channel name that allows process Amb(top) to communicate with its "child processes". ============================================================================================================================= table 7: the top part should not be in \bf but in \it table 8: I think that the first 3 summands of process Amb should be inn, outn and openn instead of ina, outa and opena. ============================================================================================================================= OK. Done. ===================================================================================================================