Separability, expressiveness, and decidability in the ambient logic
Proceedings - Symposium on Logic in Computer Science - Trang 423-432
Tóm tắt
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 (=/sub L/). We consider MA, and two Turing complete subsets of it, MA/sub IF/ and MA/sub IF//sup syn/, respectively defined by imposing a semantic and a syntactic constraint on process prefixes. The main contributions include: coinductive and inductive operational characterisations of =/sub L/; an axiomatisation of =/sub L/ on MA/sub IF//sup syn/; the construction of characteristic formulas for the processes in MA/sub IF/ with respect to =/sub L/; the decidability of =/sub L/ on MA/sub IF/ and on MA/sub IF//sup syn/, and its undecidability on MA.
Từ khóa
#Logic #Chromium #Calculus #Database languages #Switches #Computer science #Query processing #ShapeTài liệu tham khảo
10.1145/360204.375707
milner, 1989, Communication and Concurrency
milner, 1999, Communicating and Mobile Systems The ?-Calculus
10.1145/2455.2460
10.1006/inco.1996.0008
engelfriet, 1996, Multisets and structural congruence of the ?-calculus with replication
10.1016/S0019-9958(86)80031-6
charatonik, 2001, The decidability of model checking mobile ambients, Proc of CSL'01
dal-zilio, 2000, Structural congruence for ambients is decidable, LNCS, 1961
10.1006/inco.1994.1028
caires, 2002, A Spatial Logic for Concurrency (Part II)
sangiorgi, 2001, The ?-calculus A theory of mobile processes
caires, 2001, A spatial logic for concurrency (Part I), Proceedings of TACAS'01
busi, 2002, On the expressiveness of Movement in Pure Mobile Ambients
cardelli, 2001, Logical properties of name restriction, LNCS, 2044
10.1016/S1571-0661(05)80699-1
cardelli, 2001, A query language based on the ambient logic, LNCS, 2028, 1
10.1145/604264.604278
calcagno, 2001, Computability and complexity results for a spatial assertion language for data structures, LNCS, 2245
10.1145/325694.325742
10.1145/292540.292550