Abstract
In this dissertation, we study bigraphical languages—languages based on the
theory for bigraphs and bigraphical reactive systems developed by Milner
and coworkers.
We begin by examining algebraic theory for binding bigraphs. We give a
term language for binding bigraphs and develop a complete axiomatization
of structural equivalence. Along the way, we develop a set of normal form
theorems, which prove convenient for the analysis of bigraphical structure.
We examine next the central problem of matching, that is, to determine
when and where the left-hand side of a bigraphical reaction rule matches a
bigraph. We give an inductive characterization in the form of a set of rules
for inferring matching for binding bigraphs and show that the characterization
is both sound and complete.
We then develop a matching algorithm that works on terms for bigraphs.
We start by specializing the characterization above to include application
of structural congruence. We isolate a class of normal inferences, and prove
that normal inferences are sufficient for inferring all matches. The matching
algorithm relies on building normal inferences mechanically. An implementation
of the algorithm is at the core of the BPL Tool, a prototype tool for
experimenting with bigraphical reactive systems.
In a second line of work, we study bigraphical reactive systems as a vehicle
for developing a language to model biochemical reactions at the level of
cells and proteins. We discuss and isolate B,R-calculi, a family of bigraphical
reactive systems that we deem sufficient for the language. We develop
a self-contained presentation of the syntax and operational semantics for
B,R-calculi that exploits the restrictions we have made on the family. We
also treat how one may extend certain bigraphical reaction rules to include
negative contextual side-conditions. As an example, we show that the nondeterministic
-calculus (due to Danos and Laneve) can be modelled.
Finally, we build on our study above and develop a formal language, the
C-calculus, for modelling low-level interaction inside and among cells. At
the core of the calculus lies a model of formal proteins and membranes. In
addition, formal channels between compartments allow us to model an intermediate
state in cell fusion or division, regulated by diffusion. A user models
in the C-calculus by refining a set of core rules, each of which encapsulates a
core biological reaction. We illustrate the calculus with two examples, one
that models the firing of a G-protein coupled receptor protein, and another
that models the formation of clathrin-coated cytoplasmic vesicles through
budding
theory for bigraphs and bigraphical reactive systems developed by Milner
and coworkers.
We begin by examining algebraic theory for binding bigraphs. We give a
term language for binding bigraphs and develop a complete axiomatization
of structural equivalence. Along the way, we develop a set of normal form
theorems, which prove convenient for the analysis of bigraphical structure.
We examine next the central problem of matching, that is, to determine
when and where the left-hand side of a bigraphical reaction rule matches a
bigraph. We give an inductive characterization in the form of a set of rules
for inferring matching for binding bigraphs and show that the characterization
is both sound and complete.
We then develop a matching algorithm that works on terms for bigraphs.
We start by specializing the characterization above to include application
of structural congruence. We isolate a class of normal inferences, and prove
that normal inferences are sufficient for inferring all matches. The matching
algorithm relies on building normal inferences mechanically. An implementation
of the algorithm is at the core of the BPL Tool, a prototype tool for
experimenting with bigraphical reactive systems.
In a second line of work, we study bigraphical reactive systems as a vehicle
for developing a language to model biochemical reactions at the level of
cells and proteins. We discuss and isolate B,R-calculi, a family of bigraphical
reactive systems that we deem sufficient for the language. We develop
a self-contained presentation of the syntax and operational semantics for
B,R-calculi that exploits the restrictions we have made on the family. We
also treat how one may extend certain bigraphical reaction rules to include
negative contextual side-conditions. As an example, we show that the nondeterministic
-calculus (due to Danos and Laneve) can be modelled.
Finally, we build on our study above and develop a formal language, the
C-calculus, for modelling low-level interaction inside and among cells. At
the core of the calculus lies a model of formal proteins and membranes. In
addition, formal channels between compartments allow us to model an intermediate
state in cell fusion or division, regulated by diffusion. A user models
in the C-calculus by refining a set of core rules, each of which encapsulates a
core biological reaction. We illustrate the calculus with two examples, one
that models the firing of a G-protein coupled receptor protein, and another
that models the formation of clathrin-coated cytoplasmic vesicles through
budding
Originalsprog | Engelsk |
---|
Forlag | IT-Universitetet i København |
---|---|
Status | Udgivet - 2009 |