↓Skip to main content

Model Checking Mobile Ambients

Concurrency Mobile Ambients
Table of Contents

Witold Charatonik, Silvano Dal Zilio, Andrew D. Gordon, Supratik Mukhopadhyay, Jean-Marc Talbot
Theoretical Computer Science 308(1):277—331, nov 2003.

journal

 DOI〈10.1016/S0304-3975(02)00832-0〉

Abstract
#

We settle the complexity bounds of the model checking problem for the ambient calculus with public names against the ambient logic. We show that if either the calculus contains replication or the logic contains the guarantee operator, the problem is undecidable. In the case of the replication-free calculus and guarantee-free logic we prove 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
#


@Article{DalzilioS:modelcheckambient,
   author  = {Charatonik, Witold and {Dal Zilio}, Silvano and Gordon, Andrew D. and Mukhopadhyay, Supratik and Talbot, Jean-Marc},
   title   = {{Model Checking Mobile Ambients}},
   journal = {Theoretical Computer Science},
   number  = {1},
   volume  = {308},
   doi = {10.1016/S0304-3975(02)00832-0},
   pages   = {277--331},
   month   = nov, 
   year    = 2003
}