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 xiCedric LHOUSSAINE and Elisabeth REMYPart 1 Models and Data 1Chapter 1 Inference of Gene Regulatory Networks from Multi-scale Dynamic Data 3Arnaud BONNAFFOUX1.1 GRN and differentiation 41.1.1 The coordination of gene expression by GRNs 41.1.2 The process of differentiation 81.2 Inference of GRN from population data 101.2.1 Population expression data 101.2.2 Bayesian approaches 111.2.3 Information theory approaches 141.2.4 Boolean approaches 161.2.5 ODE approaches 181.3 Inferring GRNs from single-cell data 201.3.1 Single cell expression data 201.3.2 Adaptation of GRN inference algorithms for single-cell data analysis 201.3.3 Using single-cell stochastic models for GRN inference 211.4 Alternative strategies for GRN inference 251.5 Performance and limitations of GRN inference 251.6 Inference based on the wave of expression concept 271.6.1 The differentiation process seen as a dynamic process of signal processing by GRNs 281.6.2 Experimental demonstration of waves of expression 301.6.3 Using waves of expression for GRN inference 331.6.4 Scaling up the distributed computing approach 351.7 Conclusion 371.8 References 37Chapter 2 Combinatorial Optimization Problems for Studying Metabolism 45Clemence FRIOUX and Anne SIEGEL2.1 Dynamics and functionality of a metabolic network 462.1.1 Metabolic networks 462.1.2 Reconstruction of metabolic networks 472.1.3 From the dynamics of a metabolic network to its function 482.2 Understanding the metabolism of non-model organisms: metabolic gap-filling algorithms 502.2.1 Metabolism of non-model organisms 502.2.2 Reconstruction of the metabolism of non-model species and gap-filling problems 522.2.3 Added-value and limitations of metabolic gap-filling problems: example of biotic interactions 532.3 Microbiota metabolism: new optimization problems 552.3.1 Genomics of microbiota 552.3.2 From merged models to compartmentalized models 572.3.3 Completion problem for community selection in non-compartmentalized microbiota 572.3.4 Completion problem for selecting compartmentalized communities with minimal exchanges 592.4 Discrete semantics: a Boolean approximation of metabolic producibility 632.4.1 Topological accessibility of compounds and reactions in a metabolic network 642.4.2 Activation and cycles 662.4.3 Applications 672.5 Flux semantics 692.5.1 Modeling the response of a metabolic network with fluxes 702.5.2 Steady-state cycles 712.5.3 Application to the completion of metabolic networks 742.6 Comparing semantics: toward a hybrid approach 742.6.1 Complementarity of Boolean and stoichiometric abstractions 742.6.2 Hybrid completion of metabolic networks 762.7 Solving gap-filling problems with answer set programming 772.7.1 Model the Boolean activation of a reaction in ASP 782.7.2 Non-compartmentalized selection of communities 792.7.3 Compartmentalized selection of communities 802.8 Conclusion 812.9 References 81Chapter 3 The Challenges of Inferring Dynamic Models from Time Series 89Tony RIBEIRO, Maxime FOLSCHETTE, Laurent TRILLING, Nicolas GLADE, Katsumi INOUE, Morgan MAGNIN and Olivier ROUX3.1 Challenges of learning about time series 903.2 Reconstruction of a regulation network (Boolean network) and its logical rules 923.2.1 Multi-valued logic 933.2.2 Learning operations 963.2.3 Dynamical semantics 993.2.4 GULA 1033.2.5 PRIDE 1063.3 Modeling Thomas networks with delays in ASP 1103.3.1 Formalisms used 1123.3.2 Networks 1123.3.3 ASP technology 1153.3.4 Description of the problem 1163.3.5 Implementation 1183.3.6 Results 1213.3.7 Synthesis 1233.4 Promise of machine learning for biology 1243.4.1 Learning about biological regulatory networks modeling complex behaviors 1243.4.2 Review of models 1253.5 References 126Chapter 4 Connecting Logical Models to Omics Data 129Jonas BEAL, Elisabeth REMY and Laurence CALZONE4.1 Introduction 1294.2 Logical models: objectives, nature and tools 1324.2.1 Objectives and biological questions addressed 1324.2.2 Logical modeling 1334.2.3 Tools and resources for logical modeling 1354.3 Building an influence graph using biological data 1354.3.1 Defining the outline of the model 1354.3.2 Construction of the regulation network 1364.4 Defining logical rules and refining model parameters usingbiological data 1374.4.1 Determining logical rules locally 1374.4.2 Define or modify the logical model as a whole 1384.5 Data to validate models and predict behaviors 1404.6 Conclusion 1424.7 References 142Part 2 Formal and Semantic Methods 149Chapter 5 Boolean Networks: Formalism, Semantics and Complexity 151Loic PAULEVE5.1 Introduction 1515.2 Classical semantics of Boolean networks 1545.2.1 Definitions 1545.2.2 Examples 1555.2.3 Properties 1565.3 Related formalisms 1575.3.1 Cellular automata 1575.3.2 Petri nets 1575.4 Guarantees against quantitative models 1645.4.1 Boolean network refinements 1655.4.2 Counterexample for classical semantics 1675.4.3 MP Boolean networks 1685.5 Dynamic properties and complexities 1745.5.1 Fixed points 1745.5.2 Reachability between configurations 1755.5.3 Attractors 1785.6 Conclusion 1815.7 Acknowledgments 1835.8 References 183Chapter 6 Computational Logic for Biomedicine and Neurosciences 187Elisabetta DE MARIA, Joelle DESPEYROUX, Amy FELTY, Pietro LIO, Carlos OLARTE and Abdorrahim BAHRAMI6.1 Introduction 1886.2 Biomedicine in linear logic 1916.2.1 Introduction 1916.2.2 Logical frameworks, linear logic 1936.2.3 Modeling in LL 2026.2.4 Modeling breast cancer progression 2046.2.5 Verifying properties of the model 2086.2.6 Conclusion and future perspectives on the biomedicine section 2116.3 On the use of Coq to model and verify neuronal archetypes 2136.3.1 Introduction 2136.3.2 Discrete leaky integrate and fire model 2156.3.3 The basic archetypes 2176.3.4 Modeling in Coq 2176.3.5 Encoding neurons and archetypes in Coq 2206.3.6 Properties of neurons and archetypes in Coq 2246.3.7 Conclusions and future work on the archetypes section 2276.4 Conclusion and perspective 2286.5 References 230Chapter 7 The Cell: A Chemical Analog Calculator 235Francois FAGES and Franck MOLINA7.1 Introduction 2357.2 Chemical reaction networks 2377.3 Discrete dynamics and digital calculation 2397.4 Continuous dynamics and analog computation 2407.5 Turing-completeness of continuous CRNs 2437.6 Chemical compiler of calculable functions 2467.7 Chemical programming of non-living vesicles 2497.8 1014 networked analog computers 2527.9 References 253Chapter 8 Formal Verification Methods for Modeling in Biology: Biological Regulation Networks 255Gilles BERNOT, Helene COLLAVIZZA and Jean-Paul COMET8.1 Introduction 2558.1.1 Illustrative example: the simplified circadian cycle of mammals 2578.2 Formalization of Rene Thomas’s modeling 2588.2.1 Static description or influence graph 2598.2.2 Dynamics of a biological regulation graph 2618.3 Genetically modified Hoare logic 2678.3.1 Using experimental observations: an example 2688.3.2 A language of assertions 2698.3.3 A language of paths 2708.3.4 The power of assertions 2728.3.5 A logic to calculate the weakest precondition 2738.4 Temporal logic and CTL 2788.4.1 CTL and model-checking 2788.4.2 CTL fair path 2808.5 TotemBioNet 2828.5.1 Tools 2828.5.2 Example 1: growth and apoptosis of a tadpole tail 2858.5.3 Example 2: simplified mammalian cell cycle 2878.6 Hybrid formalism 2898.6.1 Hybrid regulation networks 2908.6.2 Definition of hybrid trajectories 2918.7 Hybrid Hoare logic 2988.7.1 Property, path, and assertion languages 2998.7.2 Hoare triples 3028.7.3 Weakest precondition calculus 3038.7.4 Inference rules 3048.7.5 Holmes BioNet: an implementation of the processing chain 3058.8 General methodology 3078.9 Acknowledgments 3098.10 References 310Chapter 9 Accessible Pattern Analyses in Kappa Models 313Jerome FERET9.1 Introduction 3139.1.1 Context and motivations 3139.1.2 Modeling languages for molecular interaction systems 3149.1.3 The Kappa language 3159.1.4 Abstract interpretation 3189.1.5 The Kappa ecosystem 3209.1.6 Content of the chapter 3289.2 Site graphs 3289.2.1 Signature 3289.2.2 Biochemical complexes 3309.2.3 Patterns 3329.2.4 Embedding between patterns 3349.3 Rewriting site graphs 3369.3.1 Interaction rules 3369.3.2 Reactions induced by an interaction rule 3389.3.3 Underlying reaction networks 3409.4 Analysis of reachable patterns 3429.4.1 Reachability in a reaction network 3439.4.2 Abstraction of a set of states 3459.4.3 Fixed point transfers 3509.5 Analysis using sets of orthogonal patterns 3539.5.1 Orthogonal pattern sets 3539.5.2 Post-processing and visualization of results 3599.5.3 Study of performance and practical use 3599.6 Conclusion 3629.7 References 364List of Authors 373Index 377