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.
CITATION STYLE
Charatonik, W., Dal Zilio, S., Gordon, A. D., Mukhopadhyay, S., & Talbot, J. M. (2001). The complexity of model checking mobile ambients. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2030, pp. 152–167). Springer Verlag. https://doi.org/10.1007/3-540-45315-6_10
Mendeley helps you to discover research relevant for your work.