Abstract
We settle the complexity bounds of the model checking problem for the replication-free ambient calculus with public names against the ambient logic without parallel adjunct. We show that the problem is PSPACE-complete. For the complexity upper-bound, we devise a new representation of processes that remains of polynomial size during process execution; this allows us to keep the model checking procedure in polynomial space. Moreover, we prove PSPACE-hardness of the problem for several quite simple fragments of the calculus and the logic; this suggests that there are no interesting fragments with polynomial-time model checking algorithms.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
L. Cardelli and A.D. Gordon. Mobile ambients. Theoretical Computer Science, 240:177–213, 2000.
L. Cardelli and A.D. Gordon. Types for mobile ambients. In Proceedings POPL’99, pages 79–92. ACM, 1999.
L. Cardelli and A.D. Gordon. Equational properties of mobile ambients. In Proceedings FoSSaCS’99, volume 1578 of Lecture Notes in Computer Science, pages 212–226. Springer, 1999. An extended version appears as Technical Report MSR-TR-99-11, Microsoft Research, 1999.
L. Cardelli and A.D. Gordon. Anytime, anywhere: Modal logics for mobile ambients. In Proceedings POPL’00, pages 365–377. ACM, 2000.
L. Cardelli and G. Ghelli. A query language for semistructured data based on the ambient logic. To appear in one of the proceedings volumes of ETAPS’01, to accompany an invited talk. Springer, 2001.
L. Cardelli and A.D. Gordon. Logical properties of name restriction. In ProceedingsTLCA’01. Springer, 2001. To appear.
W. Charatonik, S. Dal Zilio, A.D. Gordon, S. Mukhopadhyay, and J.-M. Talbot. The complexity of model checking mobile ambients. Technical Report MSR-TR-2001-03, Microsoft Research, 2001.
O. Kupferman, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312–360, 2000.
D. Sangiorgi. Extensionality and intensionality of the ambient logics. In Proceedings POPL’01. ACM, 2001. To appear.
W.J. Savitch. Relationships between nondeterministic and deterministic tape complexities. Journal of Computer and System Sciences, 4(2):177–192, 1970.
L.J. Stockmeyer. The polynomial-time hierarchy. Theoretical Computer Science, 3(1):1–22, 1976.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Charatonik, W., Dal Zilio, S., Gordon, A.D., Mukhopadhyay, S., Talbot, JM. (2001). The Complexity of Model Checking Mobile Ambients. In: Honsell, F., Miculan, M. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2001. Lecture Notes in Computer Science, vol 2030. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45315-6_10
Download citation
DOI: https://doi.org/10.1007/3-540-45315-6_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41864-1
Online ISBN: 978-3-540-45315-4
eBook Packages: Springer Book Archive