No CrossRef data available.
Article contents
Deciding reachability problems in Turing-complete fragments of Mobile Ambients
Published online by Cambridge University Press: 04 December 2009
Abstract
Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.
The calculus of Mobile Ambients was proposed by Cardelli and Gordon as a foundational calculus for mobile computing. Since its introduction, the computational strength and the decidability of properties have been investigated for several fragments and variants of the standard calculus. We consider the problem of reachability and characterise a public (that is, restriction-free) fragment for which it is decidable. This fragment is obtained by removing the open capability and restricting the application of the replication operator to guarded processes only. This decidability result may appear surprising in combination with the fact that the same fragment was shown to be Turing complete by Maffeis and Phillips. Finally, we extend our decidability result in two ways: we first prove the decidability of a more general property called target reachability (according to which the target of interest for the reachability analysis consists of a possibly infinite set of processes) and then show that our decidability results also hold for a more general calculus, which includes the sophisticated communication mechanisms of Boxed Ambients, which is the most relevant variant of Mobile Ambients without the open capability.
Information
- Type
- Paper
- Information
- Mathematical Structures in Computer Science , Volume 19 , Special Issue 6: Dedicated to Nadia Busi , December 2009 , pp. 1223 - 1263
- Copyright
- Copyright © Cambridge University Press 2009
References
Boneva, I. and Talbot, J.-M. (2003) When Ambients Cannot be Opened. Theoretical Computer Science 333 127–169.CrossRefGoogle Scholar
Bugliesi, M., Castagna, G. and Crafa, S. (2004) Access Control for Mobile Agents: The Calculus of Boxed Ambients. ACM Transactions on Programming Languages and Systems 26 (1)57–124.CrossRefGoogle Scholar
Busi, N. (2000) Personal communication including the proof of Turing completeness of the open-free fragment of pure MA. The extended version of this proof appears in Busi and Zavattaro (2004).Google Scholar
Busi, N. and Zavattaro, G. (2004) On the Expressive Power of Movement and Restriction in Pure Mobile Ambients. Theoretical Computer Science 322 477–515.CrossRefGoogle Scholar
Busi, N. and Zavattaro, G. (2005a) Deciding Reachability in Mobile Ambients. In: Proc. of ESOP. Springer-Verlag Lecture Notes in Computer Science 3444 248–262.CrossRefGoogle Scholar
Busi, N. and Zavattaro, G. (2005b) Reachability Analysis in Boxed Ambients. In Proc. of ICTCS. Springer-Verlag Lecture Notes in Computer Science 3701 143–159.CrossRefGoogle Scholar
Cardelli, L., Ghelli, G. and Gordon, A. D. (2002) Types for the ambient calculus. Information and Computation 177 (2)160–194.CrossRefGoogle Scholar
Cardelli, L. and Gordon, A. D. (2000a) Mobile Ambients. Theoretical Computer Science 240 (1)177–213.CrossRefGoogle Scholar
Cardelli, L. and Gordon, A. D. (2000b) Anytime, anywhere: Modal logics for mobile ambients. In: Proc. of POPL'00, ACM Press 365–377.CrossRefGoogle Scholar
Cardelli, L. and Gordon, A. D. (2005) Ambient Logic. Accepted for publication in Mathematical Structures in Computer Science.Google Scholar
Delzanno, G. and Montagna, R. (2006) On Reachability and Spatial Reachability in Fragments of BioAmbients, In: Proc. MeCBIC'06. Electronic Notes in Theoretical Computer Science 171 (2)69–79.CrossRefGoogle Scholar
Delzanno, G., Giusto, C. D., Gabbrielli, M., Laneve, C. and Zavattaro, G. (2009) The Kappa-Lattice: Decidability Boundaries for Qualitative Analysis in Biological Languages. In: Proc. of CMSB'09. Springer-Verlag Lecture Notes in Computer Science 5688 158–172.CrossRefGoogle Scholar
Danos, V. and Laneve, C. (2004) Formal molecular biology. Theoretical Computer Science 325 (1)69–110.CrossRefGoogle Scholar
Gordon, A. D. and Cardelli, L. (2002) Equational Properties of Mobile Ambients. Mathematical Structures in Computer Science 12 1–38.Google Scholar
Karp, R. M. and Miller, R. E. (1969) Parallel Program Scemata. Journal of Computer and System Sciences 3 (2)147–195.CrossRefGoogle Scholar
Levi, F. and Sangiorgi, D. (2003) Mobile Safe Ambients. ACM Transactions on Programming Languages and Systems 25 (1)1–69.CrossRefGoogle Scholar
Maffeis, S. and Phillips, I. (2004) On the Computational Strength of Pure Mobile Ambients. Theoretical Computer Science 330 501–551.CrossRefGoogle Scholar
Mayr, E. W. (1981) Persistence of Vector Replacement Systems is Decidable. Acta Informatica 15 309–318.CrossRefGoogle Scholar
Merro, M. and Hennessy, M. (2002) Bisimulation congruences in safe ambients. In: Proc. of POPL'02, ACM Press 71–80.CrossRefGoogle Scholar
Milner, R., Parrow, J. and Walker, D. (1992) A calculus of mobile processes. Information and Computation 100 1–77.CrossRefGoogle Scholar
Minsky, M. L. (1961) Recursive Unsolvability of Post's Problem of “Tag” and others Topics in the Theory of Turing Machines. Annals of Math. 74 :437–455.CrossRefGoogle Scholar
Phillips, I. and Vigliotti, M. (2002) On reduction semantics for the push and pull ambient calculus. In: Proc. of IFIP International Conference on Theoretical Computer Science (TCS'02), Kluwer 550–562.Google Scholar
Regev, A., Panina, E. M., Silverman, W., Cardelli, L. and Shapiro, E. Y. (2004) BioAmbients: an abstraction for biological compartments. Theoretical Computer Science 325 (1)141–167.CrossRefGoogle Scholar
Reisig, W. (1985) Petri nets: An Introduction, EATCS Monographs in Computer Science, Springer-Verlag.CrossRefGoogle Scholar
Shepherdson, J. C. and Sturgis, J. E. (1963) Computability of recursive functions. Journal of the ACM 10 217–255.CrossRefGoogle Scholar
Zavattaro, G. (2008) Reachability Analysis in BioAmbients. In: Proc. MeCBIC'08. Electronic Notes in Theoretical Computer Science 227 179–193.CrossRefGoogle Scholar
You have
Access
- 5
- Cited by