Symbolic Approaches to Modeling and Analysis of Biological Systems

Systems Biology is an approach to biology that involves understanding the complexity of interactions among biological entities within a systemic whole. The goal is to understand the emergence of physiological or functional properties.

Symbolic Approaches to Modeling and Analysis of Biological Systems presents contributions of formal methods from computer science for modeling the dynamics of biological systems. It deals more specifically with symbolic methods, i.e. methods that can establish the qualitative properties of models.

This book presents different approaches related to semantics, language, modeling and their link with data, and allows us to examine the fundamental problems and challenges that biological systems are facing. The first part of the book presents works that rely on various available data to build models, while the second part gathers contributions surrounding issues of semantics and formal methods.

CÉDRIC LHOUSSAINE is a professor at the Université de Lille and head of the BioComputing team at the Research Center in Computer Science, Signal and Automatic Control of Lille (CRIStAL), France.

ÉLISABETH REMY is a CNRS research director at the Mathematics Institute of Marseille and head of the Mathematics and Algorithms for Biological Systems team (MABioS) at Aix Marseille Université, France.

Preface xi

Cedric LHOUSSAINE and Elisabeth REMY

PART 1 MODELS AND DATA 1

CHAPTER 1 INFERENCE OF GENE REGULATORY NETWORKS FROM MULTI-SCALE DYNAMIC DATA 3

Arnaud BONNAFFOUX

1.1 GRN and differentiation 4

1.1.1 The coordination of gene expression by GRNs 4

1.1.2 The process of differentiation 8

1.2 Inference of GRN from population data 10

1.2.1 Population expression data 10

1.2.2 Bayesian approaches 11

1.2.3 Information theory approaches 14

1.2.4 Boolean approaches 16

1.2.5 ODE approaches 18

1.3 Inferring GRNs from single-cell data 20

1.3.1 Single cell expression data 20

1.3.2 Adaptation of GRN inference algorithms for single-cell data analysis 20

1.3.3 Using single-cell stochastic models for GRN inference 21

1.4 Alternative strategies for GRN inference 25

1.5 Performance and limitations of GRN inference 25

1.6 Inference based on the wave of expression concept 27

1.6.1 The differentiation process seen as a dynamic process of signal processing by GRNs 28

1.6.2 Experimental demonstration of waves of expression 30

1.6.3 Using waves of expression for GRN inference 33

1.6.4 Scaling up the distributed computing approach 35

1.7 Conclusion 37

1.8 References 37

CHAPTER 2 COMBINATORIAL OPTIMIZATION PROBLEMS FOR STUDYING METABOLISM 45

Clemence FRIOUX and Anne SIEGEL

2.1 Dynamics and functionality of a metabolic network 46

2.1.1 Metabolic networks 46

2.1.2 Reconstruction of metabolic networks 47

2.1.3 From the dynamics of a metabolic network to its function 48

2.2 Understanding the metabolism of non-model organisms: metabolic gap-filling algorithms 50

2.2.1 Metabolism of non-model organisms 50

2.2.2 Reconstruction of the metabolism of non-model species and gap-filling problems 52

2.2.3 Added-value and limitations of metabolic gap-filling problems: example of biotic interactions 53

2.3 Microbiota metabolism: new optimization problems 55

2.3.1 Genomics of microbiota 55

2.3.2 From merged models to compartmentalized models 57

2.3.3 Completion problem for community selection in non-compartmentalized microbiota 57

2.3.4 Completion problem for selecting compartmentalized communities with minimal exchanges 59

2.4 Discrete semantics: a Boolean approximation of metabolic producibility 63

2.4.1 Topological accessibility of compounds and reactions in a metabolic network 64

2.4.2 Activation and cycles 66

2.4.3 Applications 67

2.5 Flux semantics 69

2.5.1 Modeling the response of a metabolic network with fluxes 70

2.5.2 Steady-state cycles 71

2.5.3 Application to the completion of metabolic networks 74

2.6 Comparing semantics: toward a hybrid approach 74

2.6.1 Complementarity of Boolean and stoichiometric abstractions 74

2.6.2 Hybrid completion of metabolic networks 76

2.7 Solving gap-filling problems with answer set programming 77

2.7.1 Model the Boolean activation of a reaction in ASP 78

2.7.2 Non-compartmentalized selection of communities 79

2.7.3 Compartmentalized selection of communities 80

2.8 Conclusion 81

2.9 References 81

CHAPTER 3 THE CHALLENGES OF INFERRING DYNAMIC MODELS FROM TIME SERIES 89

Tony RIBEIRO, Maxime FOLSCHETTE, Laurent TRILLING, Nicolas GLADE, Katsumi INOUE, Morgan MAGNIN and Olivier ROUX

3.1 Challenges of learning about time series 90

3.2 Reconstruction of a regulation network (Boolean network) and its logical rules 92

3.2.1 Multi-valued logic 93

3.2.2 Learning operations 96

3.2.3 Dynamical semantics 99

3.2.4 GULA 103

3.2.5 PRIDE 106

3.3 Modeling Thomas networks with delays in ASP 110

3.3.1 Formalisms used 112

3.3.2 Networks 112

3.3.3 ASP technology 115

3.3.4 Description of the problem 116

3.3.5 Implementation 118

3.3.6 Results 121

3.3.7 Synthesis 123

3.4 Promise of machine learning for biology 124

3.4.1 Learning about biological regulatory networks modeling complex behaviors 124

3.4.2 Review of models 125

3.5 References 126

CHAPTER 4 CONNECTING LOGICAL MODELS TO OMICS DATA 129

Jonas BEAL, Elisabeth REMY and Laurence CALZONE

4.1 Introduction 129

4.2 Logical models: objectives, nature and tools 132

4.2.1 Objectives and biological questions addressed 132

4.2.2 Logical modeling 133

4.2.3 Tools and resources for logical modeling 135

4.3 Building an influence graph using biological data 135

4.3.1 Defining the outline of the model 135

4.3.2 Construction of the regulation network 136

4.4 Defining logical rules and refining model parameters using

biological data 137

4.4.1 Determining logical rules locally 137

4.4.2 Define or modify the logical model as a whole 138

4.5 Data to validate models and predict behaviors 140

4.6 Conclusion 142

4.7 References 142

PART 2 FORMAL AND SEMANTIC METHODS 149

CHAPTER 5 BOOLEAN NETWORKS: FORMALISM, SEMANTICS AND COMPLEXITY 151

Loic PAULEVE

5.1 Introduction 151

5.2 Classical semantics of Boolean networks 154

5.2.1 Definitions 154

5.2.2 Examples 155

5.2.3 Properties 156

5.3 Related formalisms 157

5.3.1 Cellular automata 157

5.3.2 Petri nets 157

5.4 Guarantees against quantitative models 164

5.4.1 Boolean network refinements 165

5.4.2 Counterexample for classical semantics 167

5.4.3 MP Boolean networks 168

5.5 Dynamic properties and complexities 174

5.5.1 Fixed points 174

5.5.2 Reachability between configurations 175

5.5.3 Attractors 178

5.6 Conclusion 181

5.7 Acknowledgments 183

5.8 References 183

CHAPTER 6 COMPUTATIONAL LOGIC FOR BIOMEDICINE AND NEUROSCIENCES 187

Elisabetta DE MARIA, Joelle DESPEYROUX, Amy FELTY, Pietro LIO, Carlos OLARTE and Abdorrahim BAHRAMI

6.1 Introduction 188

6.2 Biomedicine in linear logic 191

6.2.1 Introduction 191

6.2.2 Logical frameworks, linear logic 193

6.2.3 Modeling in LL 202

6.2.4 Modeling breast cancer progression 204

6.2.5 Verifying properties of the model 208

6.2.6 Conclusion and future perspectives on the biomedicine section 211

6.3 On the use of Coq to model and verify neuronal archetypes 213

6.3.1 Introduction 213

6.3.2 Discrete leaky integrate and fire model 215

6.3.3 The basic archetypes 217

6.3.4 Modeling in Coq 217

6.3.5 Encoding neurons and archetypes in Coq 220

6.3.6 Properties of neurons and archetypes in Coq 224

6.3.7 Conclusions and future work on the archetypes section 227

6.4 Conclusion and perspective 228

6.5 References 230

CHAPTER 7 THE CELL: A CHEMICAL ANALOG CALCULATOR 235

Francois FAGES and Franck MOLINA

7.1 Introduction 235

7.2 Chemical reaction networks 237

7.3 Discrete dynamics and digital calculation 239

7.4 Continuous dynamics and analog computation 240

7.5 Turing-completeness of continuous CRNs 243

7.6 Chemical compiler of calculable functions 246

7.7 Chemical programming of non-living vesicles 249

7.8 1014 networked analog computers 252

7.9 References 253

CHAPTER 8 FORMAL VERIFICATION METHODS FOR MODELING IN BIOLOGY: BIOLOGICAL REGULATION NETWORKS 255

Gilles BERNOT, Helene COLLAVIZZA and Jean-Paul COMET

8.1 Introduction 255

8.1.1 Illustrative example: the simplified circadian cycle of mammals 257

8.2 Formalization of Rene Thomas’s modeling 258

8.2.1 Static description or influence graph 259

8.2.2 Dynamics of a biological regulation graph 261

8.3 Genetically modified Hoare logic 267

8.3.1 Using experimental observations: an example 268

8.3.2 A language of assertions 269

8.3.3 A language of paths 270

8.3.4 The power of assertions 272

8.3.5 A logic to calculate the weakest precondition 273

8.4 Temporal logic and CTL 278

8.4.1 CTL and model-checking 278

8.4.2 CTL fair path 280

8.5 TotemBioNet 282

8.5.1 Tools 282

8.5.2 Example 1: growth and apoptosis of a tadpole tail 285

8.5.3 Example 2: simplified mammalian cell cycle 287

8.6 Hybrid formalism 289

8.6.1 Hybrid regulation networks 290

8.6.2 Definition of hybrid trajectories 291

8.7 Hybrid Hoare logic 298

8.7.1 Property, path, and assertion languages 299

8.7.2 Hoare triples 302

8.7.3 Weakest precondition calculus 303

8.7.4 Inference rules 304

8.7.5 Holmes BioNet: an implementation of the processing chain 305

8.8 General methodology 307

8.9 Acknowledgments 309

8.10 References 310

CHAPTER 9 ACCESSIBLE PATTERN ANALYSES IN KAPPA MODELS 313

Jerome FERET

9.1 Introduction 313

9.1.1 Context and motivations 313

9.1.2 Modeling languages for molecular interaction systems 314

9.1.3 The Kappa language 315

9.1.4 Abstract interpretation 318

9.1.5 The Kappa ecosystem 320

9.1.6 Content of the chapter 328

9.2 Site graphs 328

9.2.1 Signature 328

9.2.2 Biochemical complexes 330

9.2.3 Patterns 332

9.2.4 Embedding between patterns 334

9.3 Rewriting site graphs 336

9.3.1 Interaction rules 336

9.3.2 Reactions induced by an interaction rule 338

9.3.3 Underlying reaction networks 340

9.4 Analysis of reachable patterns 342

9.4.1 Reachability in a reaction network 343

9.4.2 Abstraction of a set of states 345

9.4.3 Fixed point transfers 350

9.5 Analysis using sets of orthogonal patterns 353

9.5.1 Orthogonal pattern sets 353

9.5.2 Post-processing and visualization of results 359

9.5.3 Study of performance and practical use 359

9.6 Conclusion 362

9.7 References 364

List of Authors 373

Index 377