Separability, Expressiveness, and Decidability in the Ambient Logic

• Autorzy: Hirschkoff D.
• Języki publikacji: PL

Abstrakty

EN

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 descriptive and discriminating power of AL, focusing on the equivalence on processes induced by the logic (= L ). We consider MA, and two Turing complete subsets of it, MA IF and MA synIF , respectively defined by imposing a semantic and a syntactic constraint on process prefixes. The main contributions include: coinductive and inductive operational characterisations of = L on MA synIF; an axiomatisation of = L on MA IF ; the construction of characteristic formulas for the processes in with respect to = L; the decidability of = L on MA IF and on MAsynIF , and its undecidability on MA.

Słowa kluczowe

EN

Mobile Ambients; spatial logics; modal logics; intensionality; characteristic formulas

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Schedae Informaticae
• Rocznik: 2003
• Tom: Vol. 12
• Strony: 77--84

Twórcy

autor

Hirschkoff D.

• ENS Lyon, 46 allee d'Italie, 69364 Lyon, France,

Bibliografia

• [1] Caires L., Cardelli L.; A Spatial Logic for Concurrency (Part I), in: Proc. of TACS’01, Lecture Notes in Computer Science, Springer-Verlag, 2001.
• [2] Cardelli L.: Describing Semistructured Data, SIGMOD Record, Database Principles Column, Vol. 30(4), 2001.
• [3 Cardelli L., Gordon A.; Mobile ambients, in: Proc. FoSSaCS '98, Lecture Notes in Computer Science, Springer-Verlag, Vol. 1378, 1998, pp. 140-155.
• [4] Cardelli L., Gordon A.; Types for mobile ambients, in: Proc. 26th POPL. ACM Press, 1999, pp. 79-92.
• [5] Cardelli L., Gordon A.; Anytime, anywhere: Modal logics for mobile ambients. in: Proc. 27th POPL. ACM Press, 2000.
• [6] Cardelli L., Gordon A.; Logical Properties of Name Restriction, in: Proc. of TLCA'01, Lecture Notes in Computer Science, Springer-Verlag, Vol. 2044, 2001.
• [7] Charatonik W., Talbot J.-M.; The Decidability of Model Checking Mobile Ambients, in: Proc. of CSL '01, Lecture Notes in Computer Science. Springer-Verlag, 2001.
• [8] Graf S., Sifakis J.; A modal characterization of observational congruence on finite terms of CCS, Information and Control, Vol. 68, 1986, pp. 125-145.
• [9] Hennessy M., Milner R.; Algebraic laws for nondeterminism and concurrency. Journal of the ACM, Vol. 32, 1985, pp. 137-161.
• [10] Hirschkoff D., Lozes E., Sangiorgi D.; Separability. Expressiveness and Decidability in the Ambient Logic, in this issue.
• [11] Milner R.; Communication and Concurrency, Prentice Hall. 1989.
• [12] Milner R.: Communicating and Mobile Systems: the π-Calculus, Cambridge University Press, 1999.
• [13] Sangiorgi D.; Extensionality and Intensionality of the Ambient Logic, in: Proc. of 28th POPL, ACM Press. 2001, pp. 4-17.
• [14] Sangiorgi D., Walker D.: The π-calculus: a Theory of Mobile Processes, Cambridge University Press, 2001.
• [15] Steffen B.. Ingolfsdottir A.: Characteristic formulae for processes with, divergence, Information and Computation, Vol. 110(1), 1994, pp. 149-163.