Static BiLog: a Unifying Language for Spatial Structures

• Autorzy: Conforti G. , Macedonio D. , Sassone. V.
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

bigraphs; spatial logics; context logic; separation

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 80, nr 1-3
• Strony: 91--110
• Opis fizyczny: bibliogr. 25 poz., tab.

Twórcy

autor

Conforti G.

autor

Macedonio D.

autor

Sassone. V.

• ECS, University of Southampton, UK,

Bibliografia

• [1] Birkedal, L., Debois, S., Elsborg, E., Hildebrandt, T., Niss, H.: Bigraphical Models of Context-aware Systems, FOSSACS, 2006.
• [2] Birkedal, L., Debois, S., Hildebrandt, T.: Sortings for Reactive Systems, CONCUR, 2006.
• [3] Caires, L., Cardelli, L.: A Spatial Logic for Concurrency (Part I), TACS, 2001.
• [4] Calcagno, C., Cardelli, L., Gordon, A.: Deciding Validity in a Spatial Logic for Trees, TLDI, 2003.
• [5] Calcagno, C., Gardner, P., Zarfaty, U.: A Context Logic for Tree Update, POPL, 2005.
• [6] Cardelli, L., Gardner, P., Ghelli, G.: A Spatial logic for querying graphs, ICALP, 2002.
• [7] Cardelli, L., Gardner, P., Ghelli, G.: Manipulating Trees with Hidden Labels, FOSSACS, 2003.
• [8] Cardelli, L., Gordon, A.: Ambient Logic, Mathematical Structures in Computer Science, To appear.
• [9] Conforti, G.: Spatial Logics for Semistructured Resources, PhD Thesis, Univ. of Pisa, 2005.
• [10] Conforti, G., Ghelli, G.: Decidability of Freshness, Undecidability of Revelation, FOSSACS, 2004.
• [11] Conforti, G., Macedonio, D., Sassone, V.: Bigraphical Logics for XML, SEBD, 2005.
• [12] Conforti, G., Macedonio, D., Sassone, V.: Spatial Logics for Bigraphs, ICALP, 2005.
• [13] Damgaard, T., Birkedal, L.: Axiomatizing binding bigraphs, Nordic Journal of Computing, 13(1), 2006.
• [14] Grohmann, D., Miculan, M.: Directed Bigraphs, MFPS, 2007.
• [15] Hirschkoff, D.: An Extensional Spatial Logic for Mobile Processes, CONCUR, 2004.
• [16] Jensen, O.: Forthcoming PhD Thesis, Aalborg Univ.
• [17] Jensen, O., Milner, R.: Bigraphs and mobile processes (revised), Tech. rep., Univ. of Cambridge, 2004.
• [18] Macedonio, D.: Logics for Distributed Resources, PhD Thesis, Univ. Ca' Foscari of Venice, 2006.
• [19] Milner, R.: Bigraphical Reactive Systems, CONCUR, 2001.
• [20] Milner, R.: Bigraphs for Petri nets, Lectures on Concurrency and Petri Nets: Advances in Petri Nets, 2004.
• [21] Milner, R.: Axioms for bigraphical structure, Mathematical Structures in Computer Science, 15(6), 2005.
• [22] Milner, R.: Pure bigraphs: Structure and dynamics, Information and Computation, 204(1), 2006.
• [23] O'Hearn, P., Reynolds, J., Yang, H.: Local Reasoning about Programs that Alter Data Structures, CSL, 2001.
• [24] Pitts, A.: Nominal Logic: a First Order Theory of Names and Binding, TACS, 2001.
• [25] Sangiorgi, D.: Extensionality and Intensionality of the Ambient Logic, POPL, 2001.