Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: spatial logics

Sortuj według:

Ogranicz wyniki do:

Static BiLog: a Unifying Language for Spatial Structures

Conforti G., Macedonio D., Sassone. V.

Fundamenta Informaticae

2007

Vol. 80, nr 1-3

91-110

Aiming at a unified view of the logics describing spatial structures, we introduce a general framework, BiLog, whose formulae characterise monoidal categories. As a first instance of the framework we consider bigraphs, which are emerging as a an interesting (meta-)model for spatial structures and distributed calculi. Since bigraphs are built orthogonally on two structures, a hierarchical place graph for locations and a link (hyper-)graph for connections, we obtain a logic that is a natural composition of other two instances of BiLog: a Place Graph Logic and a Link Graph Logic. We prove that these instances generalise the spatial logics for trees, for graphs and for tree contexts. We also explore the concepts of separation and sharing in these logics. We note that both the operator * of Separation Logic and the operator | of spatial logics do not completely separate the underlying structures. These two different forms of separation can be naturally derived as instances of BiLog by using the complete separation induced by the tensor product of monoidal categories along with some form of sharing.

Separability, Expressiveness, and Decidability in the Ambient Logic

Hirschkoff D.

Schedae Informaticae

2003

Vol. 12

77-84

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.