CRIS Current Research Information System
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishThe 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 |
File in questo prodotto:
Copyright © 2020