In: Foundations of Software Science and Computational Structures (FOSSACS 2003), Proceedings of the 6th International Conference (held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003), Warsaw, Poland, April 7-11, 2003, pages 169-184. Volume 2620 of Lecture Notes in Computer Science / A.D. Gordon (Ed.) --- Springer Verlag, February 2003.
Abstract: We investigate expressiveness of a fragment of the ambient calculus, a formalism for describing distributed and mobile computations. More precisely, we study expressiveness of the pure and public ambient calculus from which the capability open has been removed, in terms of the reachability problem of the reduction relation. Surprisingly, we show that even for this very restricted fragment, the reachability problem is not decidable. At a second step, for a slightly weaker reduction relation, we prove that reachability can be decided by reducing this problem to markings reachability for Petri nets. Finally, we show that the name-convergence problem as well as the model-checking problem turn out to be undecidable for both the original and the weaker reduction relation.