## Hirschkoff, Daniel and Lozes, Etienne and Sangiorgi, Davide - Separability in the Ambient Logic

lmcs:682 - Logical Methods in Computer Science, September 4, 2008, Volume 4, Issue 3
Separability in the Ambient Logic

Authors: Hirschkoff, Daniel and Lozes, Etienne and Sangiorgi, Davide

The \it{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 besides MA we consider a subcalculus in which an image-finiteness condition holds and that we prove to be Turing complete. Synchronous variants of these calculi are studied as well. In these calculi, we provide two operational characterisations of $_=L$: a coinductive one (as a form of bisimilarity) and an inductive one (based on structual properties of processes). After showing $_=L$ to be stricly finer than barbed congruence, we establish axiomatisations of $_=L$ on the subcalculus of MA (both the asynchronous and the synchronous version), enabling us to relate $_=L$ to structural congruence. We also present some (un)decidability results that are related to the above separation properties for AL: the undecidability of $_=L$ on MA and its decidability on the subcalculus.

Source : oai:arXiv.org:0806.3849
DOI : 10.2168/LMCS-4(3:4)2008
Volume: Volume 4, Issue 3
Published on: September 4, 2008
Submitted on: November 8, 2007
Keywords: Computer Science - Logic in Computer Science,Computer Science - Multiagent Systems,Computer Science - Programming Languages,F.3.2,F.4.1