Separability, expressiveness, and decidability in the ambient logic

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.