Separability, Expressiveness, and Decidability in the Ambient Logic

The Amient Logic (AL) has been proposed for expressing properties of process mobility in the calculs of Mobile Ambients (MA) and a basis for query languages on, semistructured data.We study some basic questions concerning the descriptivend discriminant power of AL, focusing on the equivalence on processess induced by logic (=L). We consider MAa, and two Tuing complete subsets of it, MAIF and MA SYNIF, respectively defined by imposing a semantic and a syntactic constraint on process prefixes. The main contributions include : conductive and inductive operational characterisations of =L; An axiomatisation of +L on MA SYNIF, the construction of characteristics formulas for the processes in MAIF with respect to =L; the decidability of +L on MAIF and on MA SYN IF and its undecidability on MALa logique des Ambients (AL) a été introduite pour expérimenter des propriétés ayant trait à la mobilité des processus dans le calcul des Ambients Mobiles(MA), ainsi qu'en tant que fondement pour des langages de requêtes pour des données semi-structurées.Nous étudions un certain nombre de questions fondamentales ayant trait au pouvoir expressif de cette logique, en bous intéressant à l'équivalence sur les processus induite par la loqique (=L). nous considérons AM, Ainsi que deux sous-ensemble Turing complets de ce calcul, MAIF et MA SYNIF, définis par les biais de restrictions syntaxique et sémantique sur les termes préfixés..Parmi nos principales contributions, nous pouvons mentionner : deux caractérisations, coinductive et inductive, de =LM; une axiomatisation de =L sur MA SYNIF ; la construction de formules caractériques pour =L pour les processus de MAIF ; la décidabilitéde =L sur MAIF et sur MAI SYNF, et la non-décidabilité de cette relation sur A