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.
Titolo: | Separability in the Ambient Logic |
Autore/i: | Daniel Hirschkoff; Etienne Lozes; SANGIORGI, DAVIDE |
Autore/i Unibo: | |
Anno: | 2008 |
Rivista: | |
Digital Object Identifier (DOI): | http://dx.doi.org/10.2168/LMCS-4(3:4)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. |
Data prodotto definitivo in UGOV: | 2010-02-01 |
Appare nelle tipologie: | 1.01 Articolo in rivista |