Separability 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 discriminating power of AL, focusing on the equivalence on processes induced by the logic (=L ). As underlying calculi we consider MA, a subcalculus called MAs in which an image-finiteness condition holds and that we prove to be Turing complete, and their synchronous variants. In these calculi, we provide operational characterisations of =L , both coinductive (as a form of bisimilarity) and inductive (based on structual properties of processes), and show that =L is stricly finer than barbed congruence. On MAs (both the asynchronous and the synchronous versions) we establish axiomatisations of =L , and then we use them to relate =L to structural congruence. We also present some (un)decidability results that are related to the above separation properties for AL: the decidability of =L on MAs , and its undecidability on MA.