The Complexity of Model Checking Mobile Ambients
- Witold Charatonik ,
- Silvano Dal Zilio ,
- Andy Gordon ,
- Supratik Mukhopadhyay ,
- Jean-Marc Talbot
Foundations of Software Science and Computation Structures |
Published by Springer, Berlin, Heidelberg
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.