Modular Languages for Systems and Synthetic Biology Michael Pedersen Doctor of Philosophy Laboratory for Foundations of Computer Science School of Informatics University of Edinburgh 2010 N V I E R D S E I F T Y O T H H G E R U U N I B Abstract Systems biology is a rapidly growing field which seeks a refined quantitative under- standing of organisms, particularly studying how molecular species such as metabo- lites, proteins and genes interact in cells to form the complex emerging behaviour exhibited by living systems. Synthetic biology is a related and emerging field which seeks to engineer new organisms for practical purposes. Both fields can benefit from formal languages for modelling, simulation and analysis. In systems biology there is however a trade-off in the landscape of existing formal languages: some are modular but may be difficult for some biologists to understand (e.g. process calculi) while others are more intuitive but monolithic (e.g. rule-based languages). The first major contribution of this thesis is to bridge this gap with a Lan- guage for Biochemical Systems (LBS). LBS is based on the modular Calculus of Bio- chemical Systems and adds e.g. parameterised modules with subtyping and a notion of nondeterminism for handling combinatorial explosion. LBS can also incorporate other rule-based languages such as Kappa, hence adding modularity to these. Modularity is important for a rational structuring of models but can also be exploited in analysis as is shown for the specific case of Petri net flows. On the synthetic biology side, none of the few existing dedicated languages allow for a high-level description of designs that can be automatically translated into DNA sequences for implementation in living cells. The second major contribution of this thesis is exactly such a language for Genetic Engineering of Cells (GEC). GEC exploits the recent advent of standard genetic parts (“biobricks”) and allows for the composition of such parts into genes in a modular and abstract manner using logical constraints. GEC programs can then be translated to DNA sequences using a constraint satisfaction engine based on a given database of genetic parts. iii Acknowledgements I thank Microsoft Research for its funding through the European PhD Scholarship Pro- gramme. I thank Gordon Plotkin for his patient supervision, and support in all things academic, over the past three years, and for his role in co-authoring two papers on LBS, one of which is incorporated into this thesis. I also thank Andrew Phillips for su- pervising me during a stimulating internship experience at Microsoft Research and for his role in co-authoring a paper on GEC which is incorporated into this thesis; many of the diagrams in Chapter 8 are entirely due to him. I thank Vincent Danos for his en- thusiasm and many inspiring discussions during and after Gordon’s sabbatical. I thank Nicolas Oury for useful discussions on LBS; Monika Heiner for useful discussions on Petri net flows; Stuart Moodie and Anatoly Sorokin for useful discussions on SBGN; William Chen for answering questions about the ErbB pathway model; and Jane Hill- ston and Luca Cardelli for useful feedback in their role as my thesis examiners. I am grateful to all my friends and colleagues in the School of Informatics who have helped make everyday life as a PhD student more fun. I am grateful to my family for always supporting me in what I want to do, even when this puts distance between us. Finally, I am grateful to Ros Marvin for her constant support and for continuing to remind me of what is truly important in life. iv Declaration I declare that this thesis was composed by myself, that the work contained herein is my own except where explicitly stated otherwise in the text, and that this work has not been submitted for any other degree or professional qualification except as specified. (Michael Pedersen) v Table of Contents 1 Introduction 1 1.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.3 Thesis outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2 Existing Formalisms for Biology 9 2.1 Petri nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.1.1 Basic Petri nets . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.1.2 Coloured Petri Nets . . . . . . . . . . . . . . . . . . . . . . . 13 2.2 Rule-based languages . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.2.1 BIOCHAM . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.2.2 BioNetGen . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.2.3 κ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.3 Rule-based Languages with Modularity . . . . . . . . . . . . . . . . 18 2.3.1 Little b . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 2.3.2 Antimony . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.4 Languages for Synthetic Biology . . . . . . . . . . . . . . . . . . . . 20 2.4.1 GenoCad . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 2.4.2 Antimony . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.5 CBS by Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.5.1 Gene Expression . . . . . . . . . . . . . . . . . . . . . . . . 23 2.5.2 A MAPK Cascade . . . . . . . . . . . . . . . . . . . . . . . 24 2.5.3 A Scaffolded MAPK Cascade. . . . . . . . . . . . . . . . . . 26 3 LBS by Example 29 3.1 Gene Expression . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3.1.1 New Species and Compartment Definitions . . . . . . . . . . 29 vii 3.1.2 Parameterised Modules . . . . . . . . . . . . . . . . . . . . . 30 3.2 A MAPK Cascade . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.2.1 Parametric Type and Subtyping . . . . . . . . . . . . . . . . 32 3.2.2 Nondeterminism . . . . . . . . . . . . . . . . . . . . . . . . 34 3.2.3 A Modification Site Type with Binding . . . . . . . . . . . . 40 3.2.4 Model Variation . . . . . . . . . . . . . . . . . . . . . . . . 43 3.3 A Scaffolded MAPK Cascade . . . . . . . . . . . . . . . . . . . . . 44 3.3.1 Species Expressions . . . . . . . . . . . . . . . . . . . . . . 44 3.3.2 Output Species Parameters . . . . . . . . . . . . . . . . . . . 46 3.4 Case Study: The Yeast Pheromone Pathway . . . . . . . . . . . . . . 47 3.4.1 Overview of the Pathway . . . . . . . . . . . . . . . . . . . . 47 3.4.2 The LBS Model . . . . . . . . . . . . . . . . . . . . . . . . 48 3.4.3 Model Validation . . . . . . . . . . . . . . . . . . . . . . . . 48 3.5 Case Study: The ErbB Pathway . . . . . . . . . . . . . . . . . . . . 49 3.5.1 Overview of the Pathway . . . . . . . . . . . . . . . . . . . . 49 3.5.2 The LBS Model . . . . . . . . . . . . . . . . . . . . . . . . 49 3.5.3 The Modelling Process and Model Validation . . . . . . . . . 50 4 The Abstract Syntax of LBS 53 4.1 Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 4.2 Compartments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 4.2.1 Compartment Expressions . . . . . . . . . . . . . . . . . . . 54 4.2.2 Derived Compartment Expressions . . . . . . . . . . . . . . 55 4.3 Species . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 4.3.1 Modification Site Expressions . . . . . . . . . . . . . . . . . 56 4.3.2 Species Expressions . . . . . . . . . . . . . . . . . . . . . . 56 4.3.3 Derived Species Expressions . . . . . . . . . . . . . . . . . . 59 4.4 Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 4.4.1 Basic Programs . . . . . . . . . . . . . . . . . . . . . . . . . 59 4.4.2 Derived Programs . . . . . . . . . . . . . . . . . . . . . . . 61 4.5 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 4.5.1 Basic Definitions . . . . . . . . . . . . . . . . . . . . . . . . 62 4.5.2 Derived Definitions . . . . . . . . . . . . . . . . . . . . . . . 62 viii 5 The General Semantics of LBS 65 5.1 Compartments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 5.1.1 Compartment Values . . . . . . . . . . . . . . . . . . . . . . 69 5.1.2 The Denotation Function . . . . . . . . . . . . . . . . . . . . 69 5.1.3 Well-Typedness of Compartment Value Lists . . . . . . . . . 70 5.1.4 Normal Forms of Compartment Value Lists . . . . . . . . . . 71 5.2 Species . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 5.2.1 Species Values . . . . . . . . . . . . . . . . . . . . . . . . . 71 5.2.2 Well-Typedness of Species Values . . . . . . . . . . . . . . . 74 5.2.3 The Denotation Function . . . . . . . . . . . . . . . . . . . . 76 5.2.4 Normal Forms of Species Values and Further Functions . . . . 80 5.2.5 Species Value Design Choices . . . . . . . . . . . . . . . . . 83 5.3 Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 5.3.1 Normal Form Reactions . . . . . . . . . . . . . . . . . . . . 84 5.3.2 The Denotation Function for Basic Programs . . . . . . . . . 86 5.3.3 The Definition of Derived Programs . . . . . . . . . . . . . . 90 5.4 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95 6 Some Concrete Semantics of LBS 99 6.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99 6.1.1 Ground Normal Form Reactions . . . . . . . . . . . . . . . . 100 6.1.2 The General Semantics in Terms of Ground Normal Form Re- actions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101 6.2 A Basic Petri Net Semantics . . . . . . . . . . . . . . . . . . . . . . 102 6.2.1 Basic Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . 102 6.2.2 The Qualitative Semantics of Basic Petri Nets . . . . . . . . . 103 6.2.3 The Concrete Basic Petri Net Semantics of LBS . . . . . . . . 104 6.3 A Coloured Petri Net Semantics . . . . . . . . . . . . . . . . . . . . 105 6.3.1 Coloured Petri Nets . . . . . . . . . . . . . . . . . . . . . . . 105 6.3.2 The Qualitative Semantics of Coloured Petri Nets . . . . . . . 106 6.3.3 The Concrete Coloured Petri Net Semantics of LBS . . . . . . 107 6.4 An ODE Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 6.4.1 ODEs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109 6.4.2 The Concrete ODE Semantics of LBS . . . . . . . . . . . . . 109 6.5 A CTMC Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 110 ix 6.5.1 CTMCs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111 6.5.2 The Concrete CTMC Semantics of LBS . . . . . . . . . . . . 111 6.6 A κ Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112 6.6.1 κ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113 6.6.2 The Concrete κ Semantics of LBS . . . . . . . . . . . . . . . 115 7 Concrete Petri Net Flow Semantics of LBS 121 7.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122 7.1.1 Flow Matrices . . . . . . . . . . . . . . . . . . . . . . . . . 122 7.1.2 Petri Net Flows . . . . . . . . . . . . . . . . . . . . . . . . . 123 7.1.3 A Running Example: Photosynthesis and Respiration . . . . . 124 7.1.4 Existing Results . . . . . . . . . . . . . . . . . . . . . . . . 126 7.2 Flow Matrix Composition and Modular Duality . . . . . . . . . . . . 127 7.2.1 Matrix-Based Composition With Place Sharing . . . . . . . . 127 7.2.2 Modular Duality: Composition With Transition Sharing . . . 128 7.3 Modular Minimal T-Flows . . . . . . . . . . . . . . . . . . . . . . . 129 7.3.1 The Intuition . . . . . . . . . . . . . . . . . . . . . . . . . . 129 7.3.2 The Definition . . . . . . . . . . . . . . . . . . . . . . . . . 130 7.3.3 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131 7.4 Modular Minimal P-Flows . . . . . . . . . . . . . . . . . . . . . . . 132 7.4.1 The Intuition . . . . . . . . . . . . . . . . . . . . . . . . . . 132 7.4.2 The Definition . . . . . . . . . . . . . . . . . . . . . . . . . 133 7.4.3 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134 7.5 Concrete Semantics of LBS . . . . . . . . . . . . . . . . . . . . . . . 135 7.5.1 The Concrete Minimal T-Flow Semantics of LBS . . . . . . . 136 7.5.2 The Concrete Minimal P-Flow Semantics of LBS . . . . . . . 138 7.5.3 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 140 7.6 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 140 8 GEC by Example 143 8.1 The Databases . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145 8.1.1 The Reaction Database . . . . . . . . . . . . . . . . . . . . . 145 8.1.2 The Parts Database . . . . . . . . . . . . . . . . . . . . . . . 145 8.1.3 Reactions Associated with Parts . . . . . . . . . . . . . . . . 147 8.2 The Basics of GEC . . . . . . . . . . . . . . . . . . . . . . . . . . . 149 8.2.1 Sequences of Typed Parts . . . . . . . . . . . . . . . . . . . 149 x