Cover -- Title Page -- Copyright -- Contents -- Foreword -- Chapter 1. Symbolic Representation and Inference of Regulatory Network Structures -- 1.1. Introduction: logical modeling and abductive inference in systems biology -- 1.2. Logical modeling of regulatory networks -- 1.2.1. Background -- 1.2.2. Logical model of signed-directed networks -- 1.2.2.1. Prior knowledge -- 1.2.2.2. Rule-based underlying model -- 1.2.2.3. Integrity constraints -- 1.2.2.4. Inferring signed-directed networks and explanatory reasoning -- 1.3. Evaluation of the ARNI approach -- 1.3.1. ARNI predictive power -- 1.3.1.1. Prediction under biological and experimental noise -- 1.3.1.2. Prediction under incomplete data -- 1.3.2. ARNI expressive power -- 1.3.2.1. Network motif representations -- 1.3.2.2. Representing complex interactions -- 1.4. ARNI assisted scientific methodology -- 1.4.1. Testing biological hypotheses -- 1.4.1.1. Testing cross-talk between signaling pathways -- 1.4.2. Informative experiments for networks discrimination -- 1.5. Related work and comparison with non-symbolic approaches -- 1.5.1. Limitations and future work -- 1.6. Conclusions -- 1.7. Bibliography -- Chapter 2. Reasoning on the Response of Logical Signaling Networks with ASP -- 2.1. Introduction -- 2.2. Answer set programming at a glance -- 2.3. Learn and control logical networks with ASP -- 2.3.1. Preliminaries -- 2.3.2. Reasoning on the response of logical networks -- 2.3.3. Learning models of immediate-early response -- 2.3.4. Minimal intervention strategies -- 2.3.5. Software toolbox: caspo -- 2.4. Conclusion -- 2.5. Acknowledgments -- 2.6. Bibliography -- Chapter 3. A Logical Model for Molecular Interaction Maps -- 3.1. Introduction -- 3.2. Biological background -- 3.3. Logical model -- 3.3.1. Activation and inhibition -- 3.3.1.1. Activation and inhibition capacities.

3.3.1.2. Relations between the activation and inhibition causes and effects -- 3.3.1.3. Relations between causal relations -- 3.3.2. Model extension -- 3.3.2.1. Phosphorylation -- 3.3.2.2. Autophosphorylation -- 3.3.2.3. Binding -- 3.3.3. Causality relations redefinition -- 3.3.3.1. Activation axioms -- 3.3.3.2. Phosphorylation axioms -- 3.3.3.3. Autophosphorylation axioms -- 3.3.3.4. Binding axioms -- 3.3.3.5. Inhibition axioms -- 3.4. Quantifier elimination for restricted formulas -- 3.4.1. Domain formulas -- 3.4.2. Restricted formulas -- 3.4.3. Completion formulas -- 3.4.4. Domain of domain formulas -- 3.4.5. Quantifier elimination procedure -- 3.5. Reasoning about interactions in metabolic interaction maps -- 3.6. Conclusion and future work -- 3.7. Acknowledgments -- 3.8. Bibliography -- Chapter 4. Analyzing Large Network Dynamics with Process Hitting -- 4.1. Introduction/state of the art -- 4.1.1. The modeling challenge -- 4.1.2. Historical context: Boolean and discrete models -- 4.1.3. Analysis issues -- 4.1.4. The process hitting framework -- 4.1.5. Outline -- 4.2. Discrete modeling with the process hitting -- 4.2.1. Motivation -- 4.2.2. The process hitting framework -- 4.2.2.1. Definition and semantics -- 4.2.3. Generalized dynamics of interaction graphs -- 4.2.3.1. Generalized dynamics of the incoherent feed-forward loop -- 4.2.4. Refining dynamics with cooperativity -- 4.2.4.1. Refined dynamics of the incoherent feed-forward loop -- 4.2.5. Relationship with Boolean/multivalued networks -- 4.2.5.1. Generalized dynamics -- 4.2.5.2. Refined dynamics -- 4.2.5.3. Discussion -- 4.3. Static analysis of discrete dynamics -- 4.3.1. Motivation -- 4.3.2. Fixed points -- 4.3.3. Abstract Interpretation using graphs of local causality -- 4.3.4. Cut sets -- 4.4. Toward a stochastic semantic -- 4.4.1. Numerical techniques.

4.4.1.1. Direct solution of the partial differential equation -- 4.4.1.2. Simulation techniques -- 4.4.2. Rates and stochastic absorption -- 4.5. Biological applications -- 4.5.1. The tool PINT -- 4.5.2. Biological examples -- 4.5.2.1. Investigating the dynamics of EGF receptor -- 4.5.2.2. Performances on large-scale networks -- 4.6. Conclusion -- 4.6.1. Assessment -- 4.6.2. Future work -- 4.7. Bibliography -- Chapter 5. ASP for Construction and Validation of Regulatory Biological Networks -- 5.1. Introduction -- 5.2. Preliminaries: ASP and biological logical networks -- 5.2.1. Answer set programming -- 5.2.2. Boolean networks and Thomas networks -- 5.3. Temporal logics -- 5.3.1. Definition of LTL and CTL -- 5.3.1.1. Linear temporal logic -- 5.3.1.2. Computational tree logic -- 5.3.2. ASP implementation of CTL and LTL -- 5.3.2.1. CTL implementation -- 5.3.2.2. LTL implementation -- 5.3.3. Example of model checking of a Boolean network -- 5.3.4. Discussion -- 5.4. ASP-based analysis of a GRN -- 5.4.1. ASP Thomas networks specification -- 5.4.1.1. Interaction graph -- 5.4.1.2. Transition graph -- 5.4.1.3. Focal state -- 5.4.1.4. Paths -- 5.4.2. Biological data modeling -- 5.4.2.1. Behaviors -- 5.4.2.2. Interaction signs -- 5.4.2.3. Mutants -- 5.4.3. Methodology for building models -- 5.4.3.1. Inconsistency repairing -- 5.4.3.2. Inference of properties -- 5.4.3.3. Minimization -- 5.4.4. Applications -- 5.4.4.1. Carbon starvation response in Escherichia coli -- 5.4.4.2. Drosophila embryo gap genes network -- 5.4.4.3. In vivo benchmarking of reverse engineering and modeling approaches interaction network -- 5.4.5. Discussion -- 5.5. Conclusions -- 5.6. Acknowledgments -- 5.7. Appendix on an advanced modeling for taking into additive constraints -- 5.7.1. Lowering the enumeration of literals.

5.7.2. Conjunction of defaults and appropriate use of the paralogical maximization operator -- 5.8. Bibliography -- Chapter 6. Simulation-based Reasoning about Biological Pathways Using Petri Nets and ASP -- 6.1. Introduction -- 6.2. Background -- 6.2.1. Answer set programming -- 6.2.2. Multiset -- 6.2.3. Petri net -- 6.3. Translating basic Petri net into ASP -- 6.3.1. An example execution -- 6.4. Changing firing semantics -- 6.5. Extension - reset arcs -- 6.6. Extension - inhibitor arcs -- 6.7. Extension - read arcs -- 6.8. Extension - colored tokens -- 6.9. Translating Petri nets with colored tokens to ASP -- 6.10. Extension - priority transitions -- 6.11. Extension - timed transitions -- 6.12. Other extensions -- 6.13. Answering simulation-based reasoning questions -- 6.13.1. Comparing altered trajectories due to reset intervention -- 6.13.2. Determining conditions leading to an observation -- 6.14. Related work -- 6.15. Conclusion -- 6.16. Bibliography -- Chapter 7. Formal Methods Applied to Gene Network Modeling -- 7.1. Introduction -- 7.2. From gene interactions to gene network modeling -- 7.2.1. Gene regulations and regulatory genes -- 7.2.2. Reverse engineering -- 7.3. Logic: a tool for multidisciplinarity with experimental sciences -- 7.3.1. What we expect from models -- 7.3.2. A logical multidisciplinary research process -- 7.4. Thomas and Sifakis should have met -- 7.4.1. Thomas' multivalued approach -- 7.4.2. Temporal logic applied to gene networks -- 7.5. Consistency of biological hypotheses -- 7.5.1. The brute force approach -- 7.5.2. Model simplifications -- 7.6. Validation of biological hypotheses -- 7.6.1. "Wet" experiments and logic formulas -- 7.6.2. Experimental strategy -- 7.7. Conclusion -- 7.8. Acknowledgments -- 7.9. Bibliography -- Chapter 8. Temporal Logic Modeling of Dynamical Behaviors: First-Order Patterns and Solvers.

8.1. Temporal logic FO-LTL(Rlin) -- 8.1.1. Syntax -- 8.1.2. Semantics: validity domains of free variables -- 8.1.3. Generic solver -- 8.1.4. Complexity -- 8.1.5. Trace simplification -- 8.1.6. Continuous satisfaction degree in [0,1] -- 8.2. Formula patterns and dedicated solvers -- 8.2.1. Temporal operator patterns -- 8.2.2. Thresholds -- 8.2.3. Amplitudes -- 8.2.4. Local maxima -- 8.2.5. Monotony -- 8.2.6. Peaks -- 8.2.7. Oscillations -- 8.3. Study case: coupled model of the cell cycle and the circadian clock -- 8.3.1. Circadian molecular clock model -- 8.3.2. Cell cycle model -- 8.3.3. Coupling of the cell cycle with the circadian clock through WEE1 -- 8.3.4. Successive peak-to-peak distances -- 8.3.5. Oscillations with precise phase shifts and imprecise amplitudes -- 8.3.6. Filtering out damped oscillations -- 8.3.7. Phase constraints -- 8.3.8. Model calibration to real data -- 8.3.9. Comparison of solvers -- 8.4. Related work -- 8.5. Conclusion -- 8.5.1. Acknowledgments -- 8.6. Bibliography -- Chapter 9. Analyzing SBGN-AF Networks Using Normal Logic Programs -- 9.1. Introduction -- 9.2. The systems biology graphical notation -- 9.3. Normal logic programs -- 9.3.1. Transformation of normal logic programs -- 9.3.1.1. Simplification rules -- 9.3.1.2. Transformation rules -- 9.4. Translation of SBGN-AF into logic programming -- 9.4.1. Special glyphs -- 9.4.2. Mapping nodes and labels to constants and translation conventions -- 9.4.3. Activity nodes -- 9.4.4. Auxiliary units -- 9.4.5. Container nodes -- 9.4.6. Modulation arcs -- 9.4.7. Logical operators -- 9.4.8. Example -- 9.4.9. Ontological axioms -- 9.4.10. Typing axioms -- 9.5. Boolean modeling of SBGN-AF signaling networks dynamics -- 9.5.1. From signaling to Boolean networks -- 9.5.2. Boolean network based on biological assumptions -- 9.5.2.1. Biological assumptions -- 9.5.2.2. Boolean network.

9.5.3. Modeling the dynamics of signaling networks in logic programing.