Paper: Separability, expressiveness, and decidability in the Ambient Logic (at LICS 2002)

Authors: Daniel Hirschkoff Étienne Lozes Davide Sangiorgi

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 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, MA1 and MA2, 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 MA2; the construction of characteristic formulas for the processes in MA1 with respect to =L; the decidability of =L on MA1 and on MA2, and its undecidability on MA.

BibTeX

  @InProceedings{HirschkoffLozesSang-Separabilityexpress,
    author = 	 {Daniel Hirschkoff and Étienne Lozes and Davide Sangiorgi},
    title = 	 {Separability, expressiveness, and decidability in the Ambient
    Logic},
    booktitle =  {Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science (LICS 2002)},
    year =	 {2002},
    month =	 {July}, 
    pages =      {423--432},
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}
  }