Separability in the Ambient Logic

Details Separability in the Ambient Logic Separability in the Ambient Logic

2008-06-24

arxiv.org/abs/0806.3849v2

LMCS 4 (3:4) 2008

Computer Science

Logic in Computer Science

logical methods in computer science, 44 pages

Scientific paper

10.2168/LMCS-4(3:4)2008

The \it{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 discriminating power of AL, focusing on the equivalence on processes induced by the logic $(=_L>)$. As underlying calculi besides MA we consider a subcalculus in which an image-finiteness condition holds and that we prove to be Turing complete. Synchronous variants of these calculi are studied as well. In these calculi, we provide two operational characterisations of $_=L$: a coinductive one (as a form of bisimilarity) and an inductive one (based on structual properties of processes). After showing $_=L$ to be stricly finer than barbed congruence, we establish axiomatisations of $_=L$ on the subcalculus of MA (both the asynchronous and the synchronous version), enabling us to relate $_=L$ to structural congruence. We also present some (un)decidability results that are related to the above separation properties for AL: the undecidability of $_=L$ on MA and its decidability on the subcalculus.

Affiliated with

Also associated with

No associations

Rating

Separability in the Ambient Logic does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Separability in the Ambient Logic, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Separability in the Ambient Logic will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-97428