Name
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 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 conductive 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. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.2168/LMCS-4(3:4)2008 | LOGICAL METHODS IN COMPUTER SCIENCE |
Keywords | DocType | Volume |
Process algebra,modal logic,Mobile Ambients,spatial logic | Journal | 4 |
Issue | ISSN | Citations |
3 | 1860-5974 | 4 |
PageRank | References | Authors |
0.48 | 20 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Étienne Lozes | 1 | 121 | 14.32 |
| Daniel Hirschkoff | 2 | 196 | 19.50 |
| Davide Sangiorgi | 3 | 2435 | 172.22 |