Extensionality and intensionality of the ambient logics

The ambient logic has been proposed for expressing properties of process mo bility in the calculus of Mobile Ambients (MA), and as a basis for query la nguages on semistructured data. To understand the extensionality and the intensionality of the logic, the e quivalence on MA processes induced by the logic (=(L)) is compared with the standard MA behavioural equivalence and with structural congruence (an int ensional equivalence, used as an auxiliary relation in the definition of sa tisfaction of the logic). The main contributions include a co-inductive cha racterisation of =(L) as a,form of labelled bisimilarity, and axiomatisatio ns of =(L) on the synchronous and asynchronous (finite) calculus. The study shows that, surprisingly, the logic allows us to observe the inte rnal structure of the processes at a very fine-grained detail, much in the same way as structural congruence does. A spin-off of the study is a better understanding of behavioural equivalence in Ambient-like calculi. For inst ance, behavioural equivalence is shown to be insensitive to stuttering phen omena originated by processes that may repeatedly enter and exit an ambient .