*For the most recent entries see the
Petri Nets Newsletter.*

## Model checking mobile ambients.

Charatonik, W.;
Dal Zilio, S.;
Gordon, A.D.;
Mukhopadhyay, S.;
Talbot, J.-M.
In:
*Theoretical Computer Science 308*, pages 277-331.
2003.

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. Morever, 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.

Keywords:
Ambient calculus; Model checking;Ambient logic; Mobile computation,
Verification.

*Do you need a refined search? Try our search engine
which allows complex field-based queries.*
*Back to the Petri Nets Bibliography*