Directed Bigraphs

We introduce directed bigraphs, a bigraphical meta-model for describing computational paradigms dealing with locations and resource communications. Directed bigraphs subsume and generalize both original Milner’s and Sassone-Sobocin ́ski’s variants of bigraphs. The key novelty is that directed bigraphs take account of the “resource request flow” inside link graphs, from controls to edges (through names), by means of the new notion of directed link graph. We give RPO and IPO constructions for this model, generalizing and unifying the constructions independently given by Jensen-Milner and Sassone-Sobocin ́ski in their respective variants. Moreover, the very same construction can be used for calculating RPBs as well, and hence also luxes (when these exist). Therefore, directed bigraphs can be used as a general theory for deriving labelled transition systems (and congruence bisimulations) from (possibly open) reactive systems.