On the Expressiveness of the Ambient Logic

摘要

The Ambient Logic (AL) has been proposed for expressing properties of processmobility in the calculus of Mobile Ambients (MA), and as a basis for querylanguages on semistructured data. In this paper, we study the expressiveness ofAL. We define formulas for capabilities and for communication in MA. We alsoderive some formulas that capture finitess of a term, name occurrences andpersistence. We study extensions of the calculus involving more complex formsof communications, and we define characteristic formulas for the equivalenceinduced by the logic on a subcalculus of MA. This subcalculus is defined byimposing an image-finiteness condition on the reducts of a MA process.