loading...
Separability, Expressiveness, and Decidability in the Ambient Logic
Copenhagen, Denmark July 22-July 25
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2002.102985017th Annual IEEE Symposium on Logic i ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Daniel Hirschkoff, LIP - ENS Lyon
Étienne Lozes, LIP - ENS Lyon

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 descriptive and discriminating power of AL, focusing on the equivalence on processes induced by the logic (=L). We consider MA, and two Turing complete subsets of it, MA_{IF} and MA_{IF}^{syn}, respectively defined by imposing a semantic and a syntactic constraint on process prefixes.

The main contributions include: coinductive and inductive operational characterisations of =L; an axiomatisation of =L on MA_{IF}^{syn}; the construction of characteristic formulas for the processes in MA_{IF} with respect to =L; the decidability of =L on MA_{IF} and on MA_{IF}^{syn}, and its undecidability on MA.

Citation:
Daniel Hirschkoff, Étienne Lozes, Davide Sangiorgi, "Separability, Expressiveness, and Decidability in the Ambient Logic," lics, pp.423, 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), 2002
Usage of this product signifies your acceptance of the Terms of Use.