Note: Cover -- Title Page -- Copyright Page -- Contents -- Preface -- Part 1. Models and Data -- Chapter 1. Inference of Gene Regulatory Networks from Multi-scale Dynamic Data -- 1.1. GRN and differentiation -- 1.1.1. The coordination of gene expression by GRNs -- 1.1.2. The process of differentiation -- 1.2. Inference of GRN from population data -- 1.2.1. Population expression data -- 1.2.2. Bayesian approaches -- 1.2.3. Information theory approaches -- 1.2.4. Boolean approaches -- 1.2.5. ODE approaches -- 1.3. Inferring GRNs from single-cell data -- 1.3.1. Single cell expression data -- 1.3.2. Adaptation of GRN inference algorithms for single-cell data analysis -- 1.3.3. Using single-cell stochastic models for GRN inference -- 1.4. Alternative strategies for GRN inference -- 1.5. Performance and limitations of GRN inference -- 1.6. Inference based on the wave of expression concept -- 1.6.1. The differentiation process seen as a dynamic process of signal processing by GRNs -- 1.6.2. Experimental demonstration of waves of expression -- 1.6.3. Using waves of expression for GRN inference -- 1.6.4. Scaling up the distributed computing approach -- 1.7. Conclusion -- 1.8. References -- Chapter 2. Combinatorial Optimization Problems for Studying Metabolism -- 2.1. Dynamics and functionality of a metabolic network -- 2.1.1. Metabolic networks -- 2.1.2. Reconstruction of metabolic networks -- 2.1.3. From the dynamics of a metabolic network to its function -- 2.2. Understanding the metabolism of non-model organisms: metabolic gap-filling algorithms -- 2.2.1. Metabolism of non-model organisms -- 2.2.2. Reconstruction of the metabolism of non-model species and gap-filling problems -- 2.2.3. Added-value and limitations of metabolic gap-filling problems: example of biotic interactions -- 2.3. Microbiota metabolism: new optimization problems. , 2.3.1. Genomics of microbiota -- 2.3.2. From merged models to compartmentalized models -- 2.3.3. Completion problem for community selection in non-compartmentalized microbiota -- 2.3.4. Completion problem for selecting compartmentalized communities with minimal exchanges -- 2.4. Discrete semantics: a Boolean approximation of metabolic producibility -- 2.4.1. Topological accessibility of compounds and reactions in a metabolic network -- 2.4.2. Activation and cycles -- 2.4.3. Applications -- 2.5. Flux semantics -- 2.5.1. Modeling the response of a metabolic network with fluxes -- 2.5.2. Steady-state cycles -- 2.5.3. Application to the completion of metabolic networks -- 2.6. Comparing semantics: toward a hybrid approach -- 2.6.1. Complementarity of Boolean and stoichiometric abstractions -- 2.6.2. Hybrid completion of metabolic networks -- 2.7. Solving gap-filling problems with answer set programming -- 2.7.1. Model the Boolean activation of a reaction in ASP -- 2.7.2. Non-compartmentalized selection of communities -- 2.7.3. Compartmentalized selection of communities -- 2.8. Conclusion -- 2.9. References -- Chapter 3. The Challenges of Inferring Dynamic Models from Time Series -- 3.1. Challenges of learning about time series -- 3.2. Reconstruction of a regulation network (Boolean network) and its logical rules -- 3.2.1. Multi-valued logic -- 3.2.2. Learning operations -- 3.2.3. Dynamical semantics -- 3.2.4. GULA -- 3.2.5. PRIDE -- 3.3. Modeling Thomas networks with delays in ASP -- 3.3.1. Formalisms used -- 3.3.2. Networks -- 3.3.3. ASP technology -- 3.3.4. Description of the problem -- 3.3.5. Implementation -- 3.3.6. Results -- 3.3.7. Synthesis -- 3.4. Promise of machine learning for biology -- 3.4.1. Learning about biological regulatory networks modeling complex behaviors -- 3.4.2. Review of models -- 3.5. References. , Chapter 4. Connecting Logical Models to Omics Data -- 4.1. Introduction -- 4.2. Logical models: objectives, nature and tools -- 4.2.1. Objectives and biological questions addressed -- 4.2.2. Logical modeling -- 4.2.3. Tools and resources for logical modeling -- 4.3. Building an influence graph using biological data -- 4.3.1. Defining the outline of the model -- 4.3.2. Construction of the regulation network -- 4.4. Defining logical rules and refining model parameters using biological data -- 4.4.1. Determining logical rules locally -- 4.4.2. Define or modify the logical model as a whole -- 4.5. Data to validate models and predict behaviors -- 4.6. Conclusion -- 4.7. References -- Part 2. Formal and Semantic Methods -- Chapter 5. Boolean Networks: Formalism, Semantics and Complexity -- 5.1. Introduction -- 5.2. Classical semantics of Boolean networks -- 5.2.1. Definitions -- 5.2.2. Examples -- 5.2.3. Properties -- 5.3. Related formalisms -- 5.3.1. Cellular automata -- 5.3.2. Petri nets -- 5.4. Guarantees against quantitative models -- 5.4.1. Boolean network refinements -- 5.4.2. Counterexample for classical semantics -- 5.4.3. MP Boolean networks -- 5.5. Dynamic properties and complexities -- 5.5.1. Fixed points -- 5.5.2. Reachability between configurations -- 5.5.3. Attractors -- 5.6. Conclusion -- 5.7. Acknowledgments -- 5.8. References -- Chapter 6. Computational Logic for Biomedicine and Neurosciences -- 6.1. Introduction -- 6.2. Biomedicine in linear logic -- 6.2.1. Introduction -- 6.2.2. Logical frameworks, linear logic -- 6.2.3. Modeling in LL -- 6.2.4. Modeling breast cancer progression -- 6.2.5. Verifying properties of the model -- 6.2.6. Conclusion and future perspectives on the biomedicine section -- 6.3. On the use of Coq to model and verify neuronal archetypes -- 6.3.1. Introduction -- 6.3.2. Discrete leaky integrate and fire model. , 6.3.3. The basic archetypes -- 6.3.4. Modeling in Coq -- 6.3.5. Encoding neurons and archetypes in Coq -- 6.3.6. Properties of neurons and archetypes in Coq -- 6.3.7. Conclusions and future work on the archetypes section -- 6.4. Conclusion and perspective -- 6.5. References -- Chapter 7. The Cell: A Chemical Analog Calculator -- 7.1. Introduction -- 7.2. Chemical reaction networks -- 7.3. Discrete dynamics and digital calculation -- 7.4. Continuous dynamics and analog computation -- 7.5. Turing-completeness of continuous CRNs -- 7.6. Chemical compiler of calculable functions -- 7.7. Chemical programming of non-living vesicles -- 7.8. 1014 networked analog computers -- 7.9. References -- Chapter 8. Formal Verification Methods for Modeling in Biology: Biological Regulation Networks -- 8.1. Introduction -- 8.1.1. Illustrative example: the simplified circadian cycle of mammals -- 8.2. Formalization of René Thomas's modeling -- 8.2.1. Static description or influence graph -- 8.2.2. Dynamics of a biological regulation graph -- 8.3. Genetically modified Hoare logic -- 8.3.1. Using experimental observations: an example -- 8.3.2. A language of assertions -- 8.3.3. A language of paths -- 8.3.4. The power of assertions -- 8.3.5. A logic to calculate the weakest precondition -- 8.4. Temporal logic and CTL -- 8.4.1. CTL and model-checking -- 8.4.2. CTL fair path -- 8.5. TotemBioNet -- 8.5.1. Tools -- 8.5.2. Example 1: growth and apoptosis of a tadpole tail -- 8.5.3. Example 2: simplified mammalian cell cycle -- 8.6. Hybrid formalism -- 8.6.1. Hybrid regulation networks -- 8.6.2. Definition of hybrid trajectories -- 8.7. Hybrid Hoare logic -- 8.7.1. Property, path, and assertion languages -- 8.7.2. Hoare triples -- 8.7.3. Weakest precondition calculus -- 8.7.4. Inference rules -- 8.7.5. Holmes BioNet: an implementation of the processing chain. , 8.8. General methodology -- 8.9. Acknowledgments -- 8.10. References -- Chapter 9. Accessible Pattern Analyses in Kappa Models -- 9.1. Introduction -- 9.1.1. Context and motivations -- 9.1.2. Modeling languages for molecular interaction systems -- 9.1.3. The Kappa language -- 9.1.4. Abstract interpretation -- 9.1.5. The Kappa ecosystem -- 9.1.6. Content of the chapter -- 9.2. Site graphs -- 9.2.1. Signature -- 9.2.2. Biochemical complexes -- 9.2.3. Patterns -- 9.2.4. Embedding between patterns -- 9.3. Rewriting site graphs -- 9.3.1. Interaction rules -- 9.3.2. Reactions induced by an interaction rule -- 9.3.3. Underlying reaction networks -- 9.4. Analysis of reachable patterns -- 9.4.1. Reachability in a reaction network -- 9.4.2. Abstraction of a set of states -- 9.4.3. Fixed point transfers -- 9.5. Analysis using sets of orthogonal patterns -- 9.5.1. Orthogonal pattern sets -- 9.5.2. Post-processing and visualization of results -- 9.5.3. Study of performance and practical use -- 9.6. Conclusion -- 9.7. References -- List of Authors -- Index -- EULA.