The Complexity of Model Checking Mobile Ambients


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.

In FoSSaCS 20014th International Conference on Foundations of Software Science and Computation Structures
  • An extended version of this paper appears in Theoretical Computer Science 308(1):277-331, Nov. 2003, under the title: Model Checking Mobile Ambients. URL

  • An extended version of this paper also appears as Technical Report MSR-TR-2001-03, Microsoft Research, May 2001. PDF