BiLog: Spatial Logics for Bigraphs
Giovanni Conforti, Damiano Macedonio, Vladimiro Sassone · ePrints Soton (University of Southampton) · 2006
Bigraphs are emerging as an interesting model for concurrent calculi, like CCS, ambients, π-calculus, and Petri nets. Bigraphs are built orthogonally on two structures: a hierarchical place graph for locations and a link (hyper-)graph for connections. Aiming at describing bigraphical structures, we introduce a general framework, BiLog, whose semantics is given by arrows in monoidal categories. We then instantiate the framework to bigraphical structures and we obtain a logic that is a natural composition of a place graph logic and a link graph logic. We explore the concepts of separation and sharing in these logics and we prove that they generalise the well known spatial logics for trees, graphs and tree contexts. The framework can be extended by introducing the dynamics in the model and a temporal modality in the logic in the usual way. However, in some interesting cases, temporal modalities can be already expressed in the static framework. To testify this, we show how to encode a minimal spatial logic for CCS in the instance of BiLog describing