Logical Interaction Networks in Biology: Theory and Application

This thesis deals with a general modeling framework for large-scale biological systems which is, on the one hand, applied to various practical instances, and on the other hand, strictly formalized and mathematically analyzed with respect to its complexity and structure.
For the biological application initially an overview of existing analytic methods for biological systems is presented, and the proposed modeling framework is classified in this context. The framework is based on logical implication formulas. It allows for the verification of a biological model, the prediction of its response to prescribed stimuli, as well as the identification of possible intervention strategies for diseases or failure modes. This basic model is afterwards extended into two directions: First, timing information of reactions in the biological unit are incorporated. This generalization additionally enables to detect possible unknown timing information or inconsistencies that arise due to modeling errors. Besides this, it provides a method to consistently integrate the logical models of related biological units into one model. Second, the purely binary basic framework is enhanced by including a fine discretization of a biological component's activity level. This permits to express different effects depending on different levels of activity of one component, and therefore the predictions of the model become more sophisticated.
On the mathematical side the logical framework and its extensions are derived and formalized. The basic model evolves to a special type of satisfiability problem (SAT) whose complexity is classified to be generally hard but mathematically easy subclasses are identified. The correspondence between SAT and integer programming is exploited and the underlying polyhedra are analyzed. Interestingly, the SAT problem allows for a wider class of polynomially solvable problems than its integer programming equivalent. Nevertheless, the computational results provided proof that the integer programming approach is computationally feasible. The basic SAT problem can additionally be translated into a bipartite digraph for which algorithms are adapted, and their practical use is discussed. Furthermore, for a special class of biological units a duality framework based on linear programming duality is derived, which completes the theory of such biological units.
The dynamic extension of the basic framework yields a related SAT problem that contains the original one as a special case, and is thus hard to solve as well. The focus for this extension is on the analysis of maximally feasible and minimally infeasible solutions of the extended SAT problem. Therefore, it is necessary to optimize over the set of solutions of the SAT problem which suggests to employ the equivalent integer programming approach. To enumerate all maximally feasible and minimally infeasible solutions the Joint Generation algorithm is utilized. To this end, a monotone reformulation of the extended SAT problem is derived that preserves the maximally feasible and minimally infeasible solutions, and at the same time significantly reduces the size of the description. In certain very restrictive cases the resulting integer optimization problems are even computationally tractable. Finally, the minimally infeasible solutions are completely characterized by means of graph structures in the original digraph, and an alternative method for computing all minimally infeasible solutions via polyhedral projection is obtained.
The discrete extension of the logical framework leads to a generalization of the SAT problem, the so called interval satisfiability problem. In this setting the variables are integer valued and associated intervals provide the set of values for which the expression becomes TRUE. To computationally determine feasible solutions, this problem is transformed to a system of polynomials which can be checked for feasibility by means of Hilbert's Nullstellensatz. Moreover, the general interval satisfiability problem is analyzed with respect to complexity and satisfiability. Concerning the computational complexity, it is shown to be generally hard even if assuming certain restrictions for the formulas. Concerning the satisfiability behavior the well known threshold phenomenon of classical random SAT, which has been observed for interval satisfiability, is examined and lower bounds on specific thresholds are identified.