↓Skip to main content

The Complexity of Model Checking Mobile Ambients

Concurrency Mobile Ambients
Table of Contents

Witold Charatonik, Silvano Dal Zilio, Andrew D. Gordon, Supratik Mukhopadhyay, Jean-Marc Talbot
In FoSSaCS 2001 — 4th International Conference on Foundations of Software Science and Computation Structures, apr 2001.

conference paper

 PDF  DOI〈10.1007/3-540-45315-6_10〉

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.

References
#

  • An extended version of this paper appears in Theoretical Computer Science 308(1):277-331, Nov. 2003, under the title: Model Checking Mobile Ambients.  Link

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

Citation
#


@InProceedings{DalzilioS:complexity,
   author    = {Charatonik, Witold and {Dal Zilio}, Silvano and Gordon, Andrew D. and Mukhopadhyay, Supratik and Talbot, Jean-Marc},
   title     = {{The Complexity of Model Checking Mobile Ambients}},
   booktitle = {FoSSaCS 2001 -- 4th International Conference on Foundations of Software Science and Computation Structures},
   series    = {Lecture Notes in Computer Science},
   volume    = {2030},
   publisher = {Springer-Verlag},
   doi = {10.1007/3-540-45315-6_10},
   pages     = {152--167},
   month     = apr, 
   year      = 2001
}