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.
Separability in the Ambient Logic
SANGIORGI, DAVIDE
2008
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
