Skip to main content
SpringerLink
Log in

Predicate μ-Calculus for Mobile Ambients

  • Published:
Journal of Computer Science and Technology Aims and scope Submit manuscript

Abstract

Ambient logics have been proposed to describe properties for mobile agents which may evolve over time as well as space. This paper takes a predicate-based approach to extending an ambient logic with recursion, yielding a predicate μ-calculus in which fixpoint formulas are formed using predicate variables. An algorithm is developed for model checking finite-control mobile ambients against formulas of the logic, providing the first decidability result for model checking a spatial logic with recursion.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Cardelli L, Gordon A. Mobile ambients. Theoretical Computer Science, Elsevier, 2000, 240: 177–213.

  2. Cardelli L, Gordon A. Anytime, anywhere: Modal logics for mobile ambients. In POPL’2000, ACM Press, Jan. 2000, pp. 365–377.

  3. Cardelli L, Gordon A. Logical Properties of Name Restriction. Typed Lambda Calculi and Applications, LNCS 2044. Springer-Verlag, 2001.

  4. Charatonik W, Talbot J M. The decidability of model checking mobile ambients. In 15th Annual Conf. European Association for Computer Science Logic, LNCS 2142, Springer-Verlag, 2001, pp. 339–354.

  5. Charatonik W, Gordon A, Talbot J M. Finite-control mobile ambients. In ESOP’02, LNCS 2305, Springer-Verlag, 2002.

  6. Winskel G. A note on model checking the modal μ-calculus. Theoretical Computer Science, Elsevier, 1991, 83: 157–167.

    Google Scholar 

  7. Cardelli L, Ghelli G. A query language based on the ambient logic. In ESOP’2001, LNCS 2028, Springer-Verlag, 2001, pp. 1–22.

  8. S Dal Zilio. Fixed points in ambient logic. In Proc. 3rd Workshop on Fixed Points in Computer Science, Sept. 2001.

  9. Luis Caires, Luca Cardeli. A spatial logic for concurrency (Part I). In TACS’2001, LNCS 2215, Springer, 2001.

  10. W Charatonik, S Dal Zilio, A Gordon et al. The complexity of model checking ambients. In FoSSaCS 2001, Honsell F, Miculan M (eds.), LNCS 2030, Springer-Verlag, 2001, pp. 152–167.

  11. Dam M. Model checking mobile processes. Information and Computation, 1996, 129: 25–51.

    Google Scholar 

  12. Luis Caires, Luca Cardeli. A spatial logic for concurrency (Part II). In CONCUR’2002, LNCS 2421, Springer, 2002.

  13. Sangiorgi D. Extensionality and intensionality of the ambient logics. In POPL’2001, ACM Press, 2001, pp. 4–13.

  14. Hirschkoff D, Lozes E, Sangiorgi D. Separability, expressiveness, and decidability in the Ambient Logic. In LICS’2002, IEEE Computer Society Press.

Download references

Author information

Authors and Affiliations

  1. Laboratory for Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, 100080, P.R. China

    Hui-Min Lin

Authors
  1. Hui-Min Lin
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hui-Min Lin.

Additional information

Supported by research grants from the National Natural Science Foundation of China (Grant No.60223005) and Chinese Academy of Sciences.

Hui-Min Lin received Ph.D. in computer science from the Institute of Software, Chinese Academy of Sciences, in 1986. He is currently a research professor at the Laboratory for Computer Science, Institute of Software, Chinese Academy of Sciences. His research interests including: process algebras, value-passing systems, model checking and modal logics, proof tools for concurrent systems, algebraic specifications, and formal methods.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Lin, HM. Predicate μ-Calculus for Mobile Ambients. J Comput Sci Technol 20, 95–104 (2005). https://doi.org/10.1007/s11390-005-0011-7

Download citation

  • Received:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11390-005-0011-7

Keywords

Search

Navigation