A first formal link between the price equation and an optimization program

The Darwin unification project is pursued. A meta-model encompassing an important class of population genetic models is formed by adding an abstract model of the number of successful gametes to the Price equation under uncertainty. A class of optimization programs are defined to represent the "individual-as-maximizing-agent analogy" in a general way. It is then shown that for each population genetic model there is a corresponding optimization program with which formal links can be established. These links provide a secure logical foundation for the commonplace biological principle that natural selection leads organisms to act as if maximizing their "fitness", provides a definition of "fitness", and clarifies the limitations of that principle. The situations covered do not include frequency dependence or social behaviour, but the approach is capable of extension.     

Automatic search for model to simulate the differentiation of T lymphocytes within the thymus

The differentiation of T Lymphocytes within the thymus is an important biological phenomenon during wich these cell acquire their functions to further control the immune system. Numerous experiments under various conditions have been devised to understand the different mechanisms involved in this complex process. Nevertheless, interpretation of these experiments lead to still contradictory debatable hypotheses. Modelisation of this process through classical simulation methods cannot be envisaged because they are not adapted to modifications of the model structure, which is the point of interest. For these reasons, we proposed a new approach of automatic search for model. The program consists of four independent connected modules : The generator produces model, based on the rationale of formal grammars. Protocol and experimental data are stored in a set of experiments. The simulator using a protocol and a model provides simulated results. Finally, the supervisor by comparing simulated results and experimental data, adapts the model parameters to increase their fit and either chooses a new experiment to explore, or modifies the model structure. Change of the model structure is performed among still unexplored models according to their promise level, which is iteratively evaluated relatively to previously explored models through a proposed model distance. The generator is written in Prolog and the other modules in C++. The architecture of the program allows us to modify or complete a module without changing anything in the other modules. As a consequence, the proposed modeling approach conceived to study T lymphocyte differentiation within the thymus remains independent of this biological phenomenon and can be applied to other biological problems.     

An automatic translation of SBML into Beta-binders

A translation of Systems Biology Markup Language (SBML) into a process algebra is proposed in order to allow the formal specification, the simulation and the formal analysis of biological models. Beta-binders, a language with a quantitative stochastic extension, is chosen for the translation. The proposed translation focuses on the main components of SBML models, as species and reactions. Furthermore, it satisfies the compositional property, i.e. the translation of the whole model is obtained by composing the translation of the subcomponents. An automatic translator tool of SBML models into Beta-binders has been implemented as well. Finally, the translation of a simple model is reported.     

From disease to development to cell biology and back

Nowadays, the focus of developmental studies is shifting away from formal models of developmental pathways that are characterised by flow charts of controlling factors connected by arrows, to mechanistic models that explain developmental processes at the cellular level. Surprisingly, this shift towards a cellular view of developmental biology is occurring simultaneously across a range of model organisms. One consequence of taking such a cell biological view of development is that many model organisms are now becoming good models for studies of human disease and therapy.     

Formal agent-based modelling of intracellular chemical interactions

Individual-based or agent-based models have proved useful in a variety of different biological contexts. This paper presents an agent-based model using a formal computational modelling approach to model a crucial biological system--the intracellular NF-kappaB signalling pathway. The pathway is vital to immune response regulation, and is fundamental to basic survival in a range of species. Alterations in pathway regulation underlie many diseases, including atherosclerosis and arthritis. Our modelling of individual molecules, receptors and genes provides a more comprehensive outline of regulatory network mechanisms than previously possible with equation-based approaches. The model has been validated with data obtained from single cell experimental analysis.     

Formal Methods for Hopfield-Like Networks

Building a meaningful model of biological regulatory network is usually done by specifying the components (e.g. the genes) and their interactions, by guessing the values of parameters, by comparing the predicted behaviors to the observed ones, and by modifying in a trial-error process both architecture and parameters in order to reach an optimal fitness. We propose here a different approach to construct and analyze biological models avoiding the trial-error part, where structure and dynamics are represented as formal constraints. We apply the method to Hopfield-like networks, a formalism often used in both neural and regulatory networks modeling. The aim is to characterize automatically the set of all models consistent with all the available knowledge (about structure and behavior). The available knowledge is formalized into formal constraints. The latter are compiled into Boolean formula in conjunctive normal form and then submitted to a Boolean satisfiability solver. This approach allows to formulate a wide range of queries, expressed in a high level language, and possibly integrating formalized intuitions. In order to explore its potential, we use it to find cycles for 3-nodes networks and to determine the flower morphogenesis regulatory network of Arabidopsis thaliana. Applications of this technique are numerous and concern the building of models from data as well as the design of biological networks possessing specified behaviors.     

Identification of bifurcation transitions in biological regulatory networks using Answer-Set Programming

Background

Numerous cellular differentiation processes can be captured using discrete qualitative models of biological regulatory networks. These models describe the temporal evolution of the state of the network subject to different competing transitions, potentially leading the system to different attractors. This paper focusses on the formal identification of states and transitions that are crucial for preserving or pre-empting the reachability of a given behaviour.

Methods

In the context of non-deterministic automata networks, we propose a static identification of so-called bifurcations, i.e., transitions after which a given goal is no longer reachable. Such transitions are naturally good candidates for controlling the occurrence of the goal, notably by modulating their propensity. Our method combines Answer-Set Programming with static analysis of reachability properties to provide an under-approximation of all the existing bifurcations.

Results

We illustrate our discrete bifurcation analysis on several models of biological systems, for which we identify transitions which impact the reachability of given long-term behaviour. In particular, we apply our implementation on a regulatory network among hundreds of biological species, supporting the scalability of our approach.

Conclusions

Our method allows a formal and scalable identification of transitions which are responsible for the lost of capability to reach a given state. It can be applied to any asynchronous automata networks, which encompass Boolean and multi-valued models. An implementation is provided as part of the Pint software, available at http://loicpauleve.name/pint.

     

Application of formal methods to biological regulatory networks: extending Thomas' asynchronous logical approach with temporal logic

Based on the discrete definition of biological regulatory networks developed by René Thomas, we provide a computer science formal approach to treat temporal properties of biological regulatory networks, expressed in computational tree logic. It is then possible to build all the models satisfying a set of given temporal properties. Our approach is illustrated with the mucus production in Pseudomonas aeruginosa. This application of formal methods from computer science to biological regulatory networks should open the way to many other fruitful applications.     

An attempt to construct a (general) mathematical framework to model biological “context-dependence”

Context-dependent nature of biological phenomena is well documented in every branch of biology. While there have been few previous attempts to (implicitly) model various (particular) facets of biological context-dependence, a formal and general mathematical construct to model the wide spectrum of context-dependence, eludes the students of biology. Such an objective model, from both ‘bottom-up’ as well as ‘top-down’ perspective, is proposed here to serve as the template to describe the various kinds of context-dependence that we encounter in different branches of biology. Interactions between biological contexts was found to be transitive but non-commutative. It is found that a hierarchical nature of dependence among the biological contexts models the emergent biological properties efficiently. Reasons for these findings are provided in a general model to describe biological reality. Scheme to algorithmically implement the hierarchic structure of organization of biological contexts was proposed with a construct named ‘Context tree’. A ‘Context tree’ based analysis of context interactions among biophysical factors influencing protein structure was performed.     

Modelling spatiotemporal olfactory data in two steps: from binary to Hodgkin-Huxley neurones

Network models of synchronously updated McCulloch-Pitts neurones exhibit complex spatiotemporal patterns that are similar to activities of biological neurones in phase with a periodic local field potential, such as those observed experimentally by Wehr and Laurent (1996, Nature 384, 162-166) in the locust olfactory pathway. Modelling biological neural nets with networks of simple formal units makes the dynamics of the model analytically tractable. It is thus possible to determine the constraints that must be satisfied by its connection matrix in order to make its neurones exhibit a given sequence of activity (see, for instance, Quenet et al., 2001, Neurocomputing 38-40, 831-836). In the present paper, we address the following question: how can one construct a formal network of Hodgkin-Huxley (HH) type neurones that reproduces experimentally observed neuronal codes? A two-step strategy is suggested in the present paper: first, a simple network of binary units is designed, whose activity reproduces the binary experimental codes; second, this model is used as a guide to design a network of more realistic formal HH neurones. We show that such a strategy is indeed fruitful: it allowed us to design a model that reproduces the Wehr-Laurent olfactory codes, and to investigate the robustness of these codes to synaptic noise.     

Modelling biological processes using workflow and Petri Net models

MOTIVATION: Biological processes can be considered at many levels of detail, ranging from atomic mechanism to general processes such as cell division, cell adhesion or cell invasion. The experimental study of protein function and gene regulation typically provides information at many levels. The representation of hierarchical process knowledge in biology is therefore a major challenge for bioinformatics. To represent high-level processes in the context of their component functions, we have developed a graphical knowledge model for biological processes that supports methods for qualitative reasoning. RESULTS: We assessed eleven diverse models that were developed in the fields of software engineering, business, and biology, to evaluate their suitability for representing and simulating biological processes. Based on this assessment, we combined the best aspects of two models: Workflow/Petri Net and a biological concept model. The Workflow model can represent nesting and ordering of processes, the structural components that participate in the processes, and the roles that they play. It also maps to Petri Nets, which allow verification of formal properties and qualitative simulation. The biological concept model, TAMBIS, provides a framework for describing biological entities that can be mapped to the workflow model. We tested our model by representing malaria parasites invading host erythrocytes, and composed queries, in five general classes, to discover relationships among processes and structural components. We used reachability analysis to answer queries about the dynamic aspects of the model. AVAILABILITY: The model is available at http://smi.stanford.edu/projects/helix/pubs/process-model/.     

Ontology-based instance data validation for high-quality curated biological pathways

Background

Modeling in systems biology is vital for understanding the complexity of biological systems across scales and predicting system-level behaviors. To obtain high-quality pathway databases, it is essential to improve the efficiency of model validation and model update based on appropriate feedback.

Results

We have developed a new method to guide creating novel high-quality biological pathways, using a rule-based validation. Rules are defined to correct models against biological semantics and improve models for dynamic simulation. In this work, we have defined 40 rules which constrain event-specific participants and the related features and adding missing processes based on biological events. This approach is applied to data in Cell System Ontology which is a comprehensive ontology that represents complex biological pathways with dynamics and visualization. The experimental results show that the relatively simple rules can efficiently detect errors made during curation, such as misassignment and misuse of ontology concepts and terms in curated models.

Conclusions

A new rule-based approach has been developed to facilitate model validation and model complementation. Our rule-based validation embedding biological semantics enables us to provide high-quality curated biological pathways. This approach can serve as a preprocessing step for model integration, exchange and extraction data, and simulation.

     

Toward verified biological models

The last several decades have witnessed a vast accumulation of biological data and data analysis. Many of these data sets represent only a small fraction of the system's behavior, making the visualization of full system behavior difficult. A more complete understanding of a biological system is gained when different types of data (and/or conclusions drawn from the data) are integrated into a larger-scale representation or model of the system. Ideally, this type of model is consistent with all available data about the system, and it is then used to generate additional hypotheses to be tested. Computer-based methods intended to formulate models that integrate various events and to test the consistency of these models with respect to the laboratory-based observations on which they are based are potentially very useful. In addition, in contrast to informal models, the consistency of such formal computer-based models with laboratory data can be tested rigorously by methods of formal verification. We combined two formal modeling approaches in computer science that were originally developed for non-biological system design. One is the inter-object approach using the language of live sequence charts (LSCs) with the Play-Engine tool, and the other is the intra-object approach using the language of statecharts and Rhapsody as the tool. Integration is carried out using InterPlay, a simulation engine coordinator. Using these tools, we constructed a combined model comprising three modules. One module represents the early lineage of the somatic gonad of C. elegans in LSCs, while a second more detailed module in statecharts represents an interaction between two cells within this lineage that determine their developmental outcome. Using the advantages of the tools, we created a third module representing a set of key experimental data using LSCs. We tested the combined statechart-LSC model by showing that the simulations were consistent with the set of experimental LSCs. This small-scale modular example demonstrates the potential for using similar approaches for verification by exhaustive testing of models by LSCs. It also shows the advantages of these approaches for modeling biology.     

基于微阵列数据的基因网络预测方法研究进展

DNA微阵列技术可同时定量测定成千上万个基因在生物样本中的表达水平,从这一技术获得的全基因组范围表达数据为揭示基因间复杂调控关系提供了可能。研究人员试图通过数学和计算方法来构建遗传互作的模型,这些基因调控网络模型有聚类法、布尔网络、贝叶斯网络、微分方程等。文章对网络重建计算方法的研究现状进行了较为全面的综述,比较了不同模型的优缺点,并对该领域进一步的研究趋势进行了展望。     

Linking physiologically-based pharmacokinetic and genome-scale metabolic networks to understand estradiol biology

Background

Estrogen is a vital hormone that regulates many biological functions within the body. These include roles in the development of the secondary sexual organs in both sexes, plus uterine angiogenesis and proliferation during the menstrual cycle and pregnancy in women. The varied biological roles of estrogens in human health also make them a therapeutic target for contraception, mitigation of the adverse effects of the menopause, and treatment of estrogen-responsive tumours. In addition, endogenous (e.g. genetic variation) and external (e.g. exposure to estrogen-like chemicals) factors are known to impact estrogen biology. To understand how these multiple factors interact to determine an individual’s response to therapy is complex, and may be best approached through a systems approach.

Methods

We present a physiologically-based pharmacokinetic model (PBPK) of estradiol, and validate it against plasma kinetics in humans following intravenous and oral exposure. We extend this model by replacing the intrinsic clearance term with: a detailed kinetic model of estrogen metabolism in the liver; or, a genome-scale model of liver metabolism. Both models were validated by their ability to reproduce clinical data on estradiol exposure. We hypothesise that the enhanced mechanistic information contained within these models will lead to more robust predictions of the biological phenotype that emerges from the complex interactions between estrogens and the body.

Results

To demonstrate the utility of these models we examine the known drug-drug interactions between phenytoin and oral estradiol. We are able to reproduce the approximate 50% reduction in area under the concentration-time curve for estradiol associated with this interaction. Importantly, the inclusion of a genome-scale metabolic model allows the prediction of this interaction without directly specifying it within the model. In addition, we predict that PXR activation by drugs results in an enhanced ability of the liver to excrete glucose. This has important implications for the relationship between drug treatment and metabolic syndrome.

Conclusions

We demonstrate how the novel coupling of PBPK models with genome-scale metabolic networks has the potential to aid prediction of drug action, including both drug-drug interactions and changes to the metabolic landscape that may predispose an individual to disease development.

     

Sparse representation approaches for the classification of high-dimensional biological data

Background

High-throughput genomic and proteomic data have important applications in medicine including prevention, diagnosis, treatment, and prognosis of diseases, and molecular biology, for example pathway identification. Many of such applications can be formulated to classification and dimension reduction problems in machine learning. There are computationally challenging issues with regards to accurately classifying such data, and which due to dimensionality, noise and redundancy, to name a few. The principle of sparse representation has been applied to analyzing high-dimensional biological data within the frameworks of clustering, classification, and dimension reduction approaches. However, the existing sparse representation methods are inefficient. The kernel extensions are not well addressed either. Moreover, the sparse representation techniques have not been comprehensively studied yet in bioinformatics.

Results

In this paper, a Bayesian treatment is presented on sparse representations. Various sparse coding and dictionary learning models are discussed. We propose fast parallel active-set optimization algorithm for each model. Kernel versions are devised based on their dimension-free property. These models are applied for classifying high-dimensional biological data.

Conclusions

In our experiment, we compared our models with other methods on both accuracy and computing time. It is shown that our models can achieve satisfactory accuracy, and their performance are very efficient.

     

Parameter Redundancy in Multistate Capture‐Recapture Models

Multistate capture‐recapture models are a powerful tool to address a variety of biological questions concerning dispersal and/or individual variability in wild animal populations. However, biologically meaningful models are often over‐parameterized and consequently some parameters cannot be estimated separately. Identifying which quantities are separately estimable is crucial for proper model selection based upon likelihood tests or information criteria and for the interpretation of the estimates obtained. We show how to investigate parameter redundancy in multistate capture‐recapture models, based on formal methods initially proposed by Catchpole and his associates for exponential family distributions (Catchpole, Freeman and Morgan, 1996. Journal of the Royal Statistical Society Series B 58, 763–774). We apply their approach to three models of increasing complexity.