Technical Report

Bigraphs are graphs whose nodes may be nested, representing locality, independently of the edges connecting them. They may be equipped with reaction rules, forming a bigraphical reactive system (Brs) in which bigraphs can reconfigure themselves. Brss aim to unify process calculi, and to model applications ---such as pervasive computing--- where locality and mobility are prominent. The paper is devoted to the theory of pure bigraphs, which underlie various more refined forms. It begins by developing a more abstract structure, a wide reactive system (Wrs), of which a Brs is an instance; in this context, labelled transitions are defined in such a way that the induced bisimilarity is a congruence