Directed Bigraphs: Theory and Applications
Davide Grohmann, Marino Miculan · 2006
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-Sobociń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. For this model we give RPO and IPO constructions, generalizing and unifying the constructions independently given by Jensen-Milner and Sassone-Sobociń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. We study also the algebraic structure of directed bigraphs: we give a sound and complete axiomatization of the (pre)category of directed bigraphs. Moreover, we use this axiomatization for encoding the λ-calculus, both in call-by-name and call-by-value variants.