Bigraphical Languages and their Simulation

We study bigraphs as a foundation for practical formal languages and
the problem of simulating such bigraphical languages. The theory of bigraphs is a foundational, graphical model of concurrent systems focusing on mobility and connectivity. It is a meta-model in the sense that it is parametrized over a signature and a set of reaction rules which determine the syntax and dynamic semantics, respectively. This allows for rather direct models and, together with a natural yet formal graphical notation and an elegant theory of behavioral equivalence, this makes bigraphs an enticing foundation for practical formal languages. However, while direct models of many process calculi have been constructed, it is unclear how suitable bigraphs are for more practical formal languages. Also, the generality of bigraphs comes at a price of complexity in the theory and simulation of bigraphical models is non-trivial. A key problem is that of matching: deciding if and how a reaction rule applies to a bigraph. In this dissertation, we study bigraphs and their simulation for two types of practical formal languages: programming languages and languages for cell biology.

First, we study programming languages and binding bigraphs, a variant of bigraphs with a facility for modeling the binders found in most programming languages. We construct and implement a provably correct term-based matching algorithm resulting in the BPL Tool, a first tool for binding bigraphs, which provides facilities for modeling, simulation, and visualization. We then employ binding bigraphs and the BPL Tool to formalize a subset of WS-BPEL, a commercial programming language for implementing business processes. We also propose and formalize an extension to WS-BPEL which supports mobile processes and process management. Finally, we identify a core subset of WS-BPEL and construct an idempotent transformation from WS-BPEL into the core subset, thereby showing that a formalization that covers the core subset is complete.

Next, we study languages for cell biology and stochastic bigraphs, an extension to bigraphs that enables modeling and analysis of stochastic behavior which is useful in cell biology. We generalize an efficient and scalable stochastic simulation algorithm for the k-calculus to bigraphs. For this purpose, we develop and implement a number of theories for (stochastic) bigraphs: a formulation of the theory that is amenable to implementation; embeddings, an alternative formulation of matches suitable for implementation; edit scripts, an alternative to reaction rules with a natural and fine-grained notion of modification; anchored matching, a localized matching algorithm; and a notion and analysis of causality at the level of rules. Finally, we develop a bigraphical language for protein-protein interaction with dynamic compartments. We elide the bigraphical underpinnings to obtain a simpler and more accessible presentation in the style of process calculi. The development is incremental, adding only the complexity necessary for each feature. We give a graphical notation which corresponds to a subset of bigraphs but is more suitable for the domain. Our approach includes a novel mechanism for handling connected components, which is necessary to model diffusion of e.g., protein-complexes. Our work suggests that two refinements of stochastic bigraphs would be convenient: connected components should be easily identifiable, and matching should be restricted to certain local contexts