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, MA_{IF} and MA_{IF}^{syn}, 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 MA_{IF}^{syn}; the construction of characteristic formulas for the processes in MA_{IF} with respect to =L; the decidability of =L on MA_{IF} and on MA_{IF}^{syn}, and its undecidability on MA.