The Ambient Logic (AL) has been proposed for expressing properties of
process mobility in the calculus of Mobile Ambients (MA), and as a
basis for query languages on semistructured data.
We study some basic questions concerning the descriptive and
discriminating power of AL, focusing on the equivalence on processes
induced by the logic (=L). We consider MA, and two Turing complete
subsets of it, MA1 and MA2, respectively defined by imposing a
semantic and a syntactic constraint on process prefixes.
The main contributions include: coinductive and inductive operational
characterisations of =L; an axiomatisation of =L on MA2; the
construction of characteristic formulas for the processes in MA1 with
respect to =L; the decidability of =L on MA1 and on MA2, and its
undecidability on MA.
