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.
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11585/82976
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 31
  • ???jsp.display-item.citation.isi??? 0
social impact