A Novel Method to Verify Multilevel Computational Models of Biological Systems Using Multiscale Spatio-Temporal Meta Model Checking

Verifiable biology

The formalization of biological systems using computational modelling approaches as an alternative to mathematical-based methods has recently received much interest because computational models provide a deeper mechanistic understanding of biological systems. In particular, formal verification, complementary approach to standard computational techniques such as simulation, is used to validate the system correctness and obtain critical information about system behaviour. In this study, we survey the most frequently used computational modelling approaches and formal verification techniques for computational biology. We compare a number of verification tools and software suites used to analyse biological systems and biochemical networks, and to verify a wide range of biological properties. For users who have no expertise in formal verification, we present a novel methodology that allows them to easily apply formal verification techniques to analyse their biological or biochemical system of interest.

Virtual Transcriptomics: Noninvasive Phenotyping of Atherosclerosis by Decoding Plaque Biology From Computed Tomography Angiography Imaging

[Figure: see text].

N-PAT: A Nested Model-Checker

N-PAT is a new model-checking tool that supports the verification of nested-models, i.e. models whose behaviour depends on the results of verification tasks. In this paper, we describe its operation and discuss mechanisms that are tailored to the efficient verification of nested-models. Further, we motivate the advantages of N-PAT over traditional model-checking tools through a network security case study.

Coloured Petri nets for multilevel, multiscale and multidimensional modelling of biological systems

Owing to the availability of data of one biological phenomenon at different levels/scales, modelling of biological systems is moving from single level/scale to multiple levels/scales, which introduces a number of challenges. Coloured Petri nets (ColPNs) have been successfully applied to multilevel, multiscale and multidimensional modelling of some biological systems, addressing many of these challenges. In this article, we first review the basics of ColPNs and some popular extensions, and then their applications for multilevel, multiscale and multidimensional modelling of biological systems. This understanding of how to use ColPNs for modelling biological systems will assist readers in selecting appropriate ColPN classes for specific modelling circumstances.

An Integrative Analysis of Time-varying Regulatory Networks From High-dimensional Data

Directed networks have been widely used to describe many biological processes and functions. Understanding the structure of biological networks, especially regulatory networks, could help discover the mechanisms underlying important biological processes and pathogenesis of diseases. Most network inference methods assume the network structure is time-invariant or stationary. However, in some processes, the network structure is non-stationary or time-varying. The stationary network inference methods might not be able to directly used to reconstruct time-varying networks. Some non-stationary network learning methods have been proposed to infer the networks, but, the inferred networks are not regulatory networks which require activation and inhibition information. This work proposes an integrative approach, which combines the changepoint estimation, weighted network learning and searching, and model checking technique, to reconstruct time varying regulatory networks from high-dimensional time series data. We illustrate this approach to study the structure changes of Drosophila's regulatory networks in its life cycle.

Formal reasoning about systems biology using theorem proving

System biology provides the basis to understand the behavioral properties of complex biological organisms at different levels of abstraction. Traditionally, analysing systems biology based models of various diseases have been carried out by paper-and-pencil based proofs and simulations. However, these methods cannot provide an accurate analysis, which is a serious drawback for the safety-critical domain of human medicine. In order to overcome these limitations, we propose a framework to formally analyze biological networks and pathways. In particular, we formalize the notion of reaction kinetics in higher-order logic and formally verify some of the commonly used reaction based models of biological networks using the HOL Light theorem prover. Furthermore, we have ported our earlier formalization of Zsyntax, i.e., a deductive language for reasoning about biological networks and pathways, from HOL4 to the HOL Light theorem prover to make it compatible with the above-mentioned formalization of reaction kinetics. To illustrate the usefulness of the proposed framework, we present the formal analysis of three case studies, i.e., the pathway leading to TP53 Phosphorylation, the pathway leading to the death of cancer stem cells and the tumor growth based on cancer stem cells, which is used for the prognosis and future drug designs to treat cancer patients.

Systems Medicine-Complexity Within, Simplicity Without

This paper presents a brief history of Systems Theory, progresses to Systems Biology, and its relation to the more traditional investigative method of reductionism. The emergence of Systems Medicine represents the application of Systems Biology to disease and clinical issues. The challenges faced by this transition from Systems Biology to Systems Medicine are explained; the requirements of physicians at the bedside, caring for patients, as well as the place of human-human interaction and the needs of the patients are addressed. An organ-focused transition to Systems Medicine, rather than a genomic-, molecular-, or cell-based effort is emphasized. Organ focus represents a middle-out approach to ease this transition and to maximize the benefits of scientific discovery and clinical application. This method manages the perceptions of time and space, the massive amounts of human- and patient-related data, and the ensuing complexity of information.