A CSP implementation of the bigraph embedding problem

Bigraphical Reactive Systems (BRSs) [14, 20] are a flexible and expressive meta-model for ubiquitous computation. System states are represented by bigraphs, which are compositional data structures describing at once both the locations and the logical connections of (possibly nested) components of a system. Like graph rewriting [25], the dynamic behaviour of a system is defined by a set of (parametric) reaction rules, which can modify a bigraph by replacing a redex with a reactum, possibly changing agents' positions and connections. BRSs have been successfully applied to the formalization of a broad variety of domain-specific calculi and models, from traditional programming languages to process calculi for concurrency and mobility, from context-aware systems to web-service orchestration languages, from business processes to systems biology; a non exhaustive list is [2,4,5,8,16,19]. Very recently bigraphs have been used in structure-aware agent-based computing for modelling the structure of the (physical) world where the agents operates (e.g., drones, robots, etc.) [21]. Beside their normative and expressive power, BRSs are appealing because they provide a range of interesting general results and tools, which can be readily instantiated with the specific model under scrutiny: simulation tools, systematic construction of compositional bisimulations [14], graphical editors [9], general model checkers [24], modular composition [23], stochastic extensions [15], etc. In this paper, we give an implementation for a crucial problem that virtually all these tools have to deal with, i.e., the matching a bigraph inside an agent. Roughly, this can be stated as follows: given R and A, we have to find (all, or some) C,D such that A C R D. Clearly this is required by any simulation tool (in order to apply a reaction rule, we have to match the redex inside the agent, and then replace it with the reactum), but also in other tools, e.g., for implementing "find&replace" in graphical editors, for occurrence checks in sortings [1] and model checkers, for refinements in architectural design tools, etc. 1