On the Expressiveness of the Ambient Logic

TL;DR

This paper investigates the expressive power of the Ambient Logic in describing process mobility, communication, and properties like finiteness within the Mobile Ambients calculus, including extensions and characteristic formulas.

Contribution

It introduces formulas for capabilities and communication, explores extensions with complex communications, and defines characteristic formulas for a subcalculus of Mobile Ambients.

Findings

Formulas for capabilities and communication in MA

Characterization of finiteness and persistence properties

Extension of the calculus with complex communication forms

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. In this paper, we study the expressiveness of AL. We define formulas for capabilities and for communication in MA. We also derive some formulas that capture finitess of a term, name occurrences and persistence. We study extensions of the calculus involving more complex forms of communications, and we define characteristic formulas for the equivalence induced by the logic on a subcalculus of MA. This subcalculus is defined by imposing an image-finiteness condition on the reducts of a MA process.