BACKGROUND: Integrating genome-wide gene expression patient profiles with regulatory knowledge is a challenging task because of the inherent heterogeneity, noise and incompleteness of biological data. From the computational side, several solvers for logic programs are able to perform extremely well in decision problems for combinatorial search domains. The challenge then is how to process the biological knowledge in order to feed these solvers to gain insights in a biological study. It requires formalizing the biological knowledge to give a precise interpretation of this information; currently, very few pathway databases offer this possibility. RESULTS: The presented work proposes an automatic pipeline to extract automatically regulatory knowledge from pathway databases and generate novel computational predictions related to the state of expression or activity of biological molecules. We applied it in the context of hepatocellular carcinoma (HCC) progression, and evaluate the precision and the stability of these computational predictions. Our working base is a graph of 3383 nodes and 13,771 edges extracted from the KEGG database, in which we integrate 209 differentially expressed genes between low and high aggressive HCC across 294 patients. Our computational model predicts the shifts of expression of 146 initially non-observed biological components. Our predictions were validated at 88% using a larger experimental dataset and cross-validation techniques. In particular, we focus on the protein complexes predictions and show for the first time that NFKB1/BCL-3 complexes are activated in aggressive HCC. In spite of the large dimension of the reconstructed models, our analyses over the computational predictions discover a well constrained region where KEGG regulatory knowledge constrains gene expression of several biomolecules. These regions can offer interesting windows to perturb experimentally such complex systems. CONCLUSION: This new pipeline allows biologists to develop their own predictive models based on a list of genes. It facilitates the identification of new regulatory biomolecules using knowledge graphs and predictive computational methods. Our workflow is implemented in an automatic python pipeline which is publicly available at https://github.com/LokmaneChebouba/key-pipeand contains as testing data all the data used in this paper.

Learning from interpretation transition (LFIT) automatically constructs a model of the dynamics of a system from the observation of its state transitions. So far, the systems that LFIT handles are restricted to discrete variables or suppose a discretization of continuous data. However, when working with real data, the discretization choices are critical for the quality of the model learned by LFIT . In this paper, we focus on a method that learns the dynamics of the system directly from continuous time-series data. For this purpose, we propose a modeling of continuous dynamics by logic programs composed of rules whose conditions and conclusions represent continuums of values.

We present a new hybrid Hoare logic dedicated for a class of linear hybrid automata well suited to model gene regulatory networks. These automata rely on Thomas' discrete framework in which qualitative parameters have been replaced by continuous parameters called celerities. The identification of these parameters remains one of the keypoints of the modelling process, and is difficult especially because the modelling framework is based on a continuous time. We introduce Hoare triples which handle biological traces and pre/post-conditions. Observed chronometrical biological traces play the role of an imperative program for classical Hoare logic and our hybrid Hoare logic, defined by inference rules, is proved to be sound. Furthermore, we present a weakest precondition calculus (a la Dijkstra) which leads to constraints on dynamical parameters. Finally, we illustrate our "constraints generator" with a simplified circadian clock model describing the rhythmicity of cells in mammals on a 24-hour period.

The combination of numerous simple influences between the components of a Biological Regulatory Network (BRN) often leads to behaviors that cannot be grasped intuitively. They thus call for the development of proper mathematical methods to delineate their dynamical properties. As a consequence, formal methods and computer tools for the modeling and simulation of BRNs become essential. Our recently introduced discrete formalism called the Process Hitting (PH), a restriction of synchronous automata networks, is notably suitable to such study. In this paper, we propose a new logical approach to perform model-checking of dynamical properties of BRNs modeled in PH. Our work here focuses on state reachability properties on the one hand, and on the identification of fixed points on the other hand. The originality of our model-checking approach relies in the exhaustive enumeration of all possible simulations verifying the dynamical properties thanks to the use of Answer Set Programming.